Unfolding Expressions for Gradual Verification
summary
Formalizes evaluation and proof obligations for unfolding expressions in gradual verification, giving both static (isorecursive) and dynamic (equirecursive) semantics and extending the progress–preservation soundness proof that targets any verifier built on Viper. Implements symbolic-evaluation rules (produce/consume, eval/exec) for unfold/fold, handles nontermination by depth-cutoff to a symbolic summary, and uncovers an implementation soundness bug during validation; aims to justify unfolding in real systems like Gobra and C0 frontends.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:46Viper verification
- 3:10Recursive predicates
- 4:56Linked list example
- 8:06Unfolding in programs
- 9:52Why formalize
- 10:34Gradual verification
- 13:01Framing specifications
- 14:04Formal semantics
- 16:56Unbounded recursion
- 18:17Isor vs equi-recursive
- 19:21Predicates in proofs
- 20:03Future work
- 21:09Long-term vision
- 22:14Q&A
related talks
15mGradual Verification of Recursive Heap Data Structures
01h 05mVerifying Infinitely Many Programs at Once
19mPredictable Verification using Intrinsic Definitions
23mSpecifying and Verifying Future Conditions
24mProving False in Object Oriented Verification Programs by Exploiting Non-Termination
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
15mIncremental Certified Programming