FO-Complete Program Verification for Heap Logics
summary
Claims a practical verification pipeline that achieves FO-Complete reasoning for heap logics by designing two logics — frame logic (FL) and SL-FL — with implicit heaplets and support operators to avoid second‑order heap quantification. Builds a VC generator that reduces annotated programs to FO + least‑fixed‑points, uses thrifty unfolding, quantifier instantiation and SMT solvers, and implements tools evaluated on linked‑structure benchmarks; all benchmarks verify in under a minute with FL consistently faster, demonstrating the approach works.
AI-written summary · about
chapters (9)
- 0:00FO-complete heap verification
- 1:06Incompleteness in heap logics
- 2:49FO-completeness and fixed points
- 4:36Designing FO-complete logics
- 5:38Frame logic properties
- 7:27Verification condition generation
- 9:11Separation logic SLFL semantics
- 10:57Benchmark results and performance
- 11:17Conclusion and future work
related talks
01h 05mVerifying Infinitely Many Programs at Once
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
23mSeparating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
19mPredictable Verification using Intrinsic Definitions
22mExecution Time Program Verification With Tight Bounds
23mSpecifying and Verifying Future Conditions
52mThink Abstractly, Work Concretely
15mGradual Verification of Recursive Heap Data Structures