Data Abstraction: A General Framework to Handle Program Verification of Data Structures
summary
Proposes a constructive reduction that turns universally quantified array properties like “all elements below index i are nonzero” into a purely scalar invariant search problem so existing scalar analyzers can be reused. The framework operates on Horn formulas and supplies a relative completeness resolution scheme: the reduced scalar problem has a solution if and only if the original array property is expressible in the chosen abstraction. Includes a formal proof of equivalence and a concrete algorithm for generating the scalar verification obligations.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 0:13Goal
- 0:44Structure
- 1:13Array initialization
- 1:51Frontend
- 2:29Example
- 3:59Logical Formula
- 4:35Motivation
- 5:08Formalization
- 5:53Array Abstraction
- 6:24Information Loss
- 8:59Abstract Algorithm
- 9:34Abstract Algorithm Example
- 11:09Technical Work
- 11:44Conclusion
related talks
01h 05mVerifying Infinitely Many Programs at Once
21mMechanised Hypersafety Proofs about Structured Data
58mA New Perspective on Commutativity in Verification
17mA HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…)
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
52mThink Abstractly, Work Concretely
19mPredictable Verification using Intrinsic Definitions
22mA Categorical Basis for Robust Program Analysis