Gradual Verification: Assuring Software Incrementally
summary
Proposes gradual verification that lets each assertion be complete, partial, or omitted and gives a sound mix of static and runtime checks so every spec violation is caught either statically or at runtime. Verifies first‑order specs over recursive mutable heaps, implements fold/unfold and ownership via implicit dynamic frames, and resolves iso‑ vs equi‑recursive predicate mismatches. Prototype tool is built on Viper; empirical point: memory‑safety emerges after ~13 annotation lines (~40% of checks) and a full spec yields 100% static verification.
AI-written summary · about
chapters (9)
- 0:00Gradual verification intro
- 2:51Why gradual verification matters
- 5:25Dynamic vs static trade-offs
- 8:13How gradual verification works
- 11:50Ownership in verification
- 16:31Dynamic ownership execution
- 20:23Recursive predicates and runtime checks
- 22:09Restricting ownership in code
- 23:14Implementation and future
related talks
15mGradual Verification of Recursive Heap Data Structures
19mPredictable Verification using Intrinsic Definitions
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
15mIncremental Certified Programming
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
23mSpecifying and Verifying Future Conditions
16mPreguss: It Analyzes, It Specifies, It Verifies
20mVerification-Preserving Inlining in Automatic Separation Logic Verifiers