Gradual Verification of Recursive Heap Data Structures
summary
Practical system that extends a base static verifier with gradual formulas and optimistic strengthening, inserting runtime checks when a missing spec was assumed; targets recursive heap structures (lists, trees, graphs) and supports equi-recursive predicates checked as recursive boolean functions. Example: inserting at head of a list uses accessibility predicates and an ownership set tracked at runtime. Empirical increments: 13 lines of specs yield 40% of VCs statically, 22 lines yield 86%, 44 lines reach full static; a prototype is being implemented.
AI-written summary · about
chapters (13)
- 0:00Intro
- 0:23Dynamic verification increases runtime overhead for weaker assurances
- 1:34Naive Verification Attempt: Missing Preconditions
- 2:00Naive Verification Attempt: Missing Lemmas
- 2:10Naive Verification Attempt: Missing Specifications
- 2:38Gradual Verification to the Rescue
- 3:38Incremental Static Verification of List Insertion
- 4:46Gradual Verification Framework [Bader et al.'18]
- 6:05Extending the prior Gradual Verification Approach
- 6:52Giving the Right Meaning to Imprecise Formulas
- 7:32Meaning of Imprecise Formulas: By Example
- 10:54Run-time checking
- 12:29Dynamically Verifying Accessibility Predicates
related talks
28mGradual Verification: Assuring Software Incrementally
19mPredictable Verification using Intrinsic Definitions
15mEvaluating Soundness of a Gradual Verifier with Property Based Testing
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
26mUnfolding Expressions for Gradual Verification
27mCompositional Verification of Concurrent C Programs with Search Structure Templat...
23mSpecifying and Verifying Future Conditions
18mPreview: Verification (Correctness)