Predictable Verification using Intrinsic Definitions
summary
Proposes that defining heap structures with intrinsic definitions — auxiliary monadic maps plus local constraints — makes verification decidable and therefore predictable, replacing recursive specs. Verification uses explicit ghost code that updates maps in a “fix‑what‑you‑break” style; they implement it in Boogie, verify many tree and list routines including a linked‑list + BST overlay, report annotation cost ≈1:2.5 LOC and second‑scale VC times, and publish reusable artifacts.
AI-written summary · about
chapters (13)
- 0:00Predictable verification intro
- 2:27Traditional verification frustrations
- 3:10Intrinsic definitions intro
- 5:59Verification with ghost code
- 7:22Broken nodes and impact sets
- 9:09Decidable verification conditions
- 10:54Advantages over recursion
- 11:15Expressiveness and efficiency eval
- 12:17Overlay data structures case study
- 13:20Annotation burden and automation
- 14:01Intrinsic definitions summary
- 14:43Future directions
- 15:44Q&A
related talks
15mGradual Verification of Recursive Heap Data Structures
28mGradual Verification: Assuring Software Incrementally
12mFO-Complete Program Verification for Heap Logics
27mCompositional Verification of Concurrent C Programs with Search Structure Templat...
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
01h 05mVerifying Infinitely Many Programs at Once
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination
13mA Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs