Separating the Wheat from the Chaff: Understanding (In-)Completeness of Proof(…)
summary
Main claim: the common fold/unfold proof steps are sound and — for the quantifier‑free, theory‑free fragment — complete for a weaker semantics called Weak Separation Logic (WSL), so every failure of fold/unfold corresponds to a WSL countermodel. Method: a model‑preserving translation from WSL to first‑order logic and use of symbolic structures (summary nodes) to represent infinite fixed‑point countermodels. Prototype translates SLS benchmarks (≈700 entailments) to FOL and finds rogue countermodels for 92% of one benchmark partition; the EDH fragment admits a complete FOL‑based proof mechanism.
AI-written summary · about
chapters (13)
- 0:00Introduction
- 1:08Separation logic
- 2:55Incompleteness in separation logic
- 3:59Cyclic list segment example
- 6:09Fold/unfold failures
- 7:57Weak separation logic
- 10:25Rogue counter models
- 12:54Finding rogue models
- 15:26Completeness of fold/unfold
- 17:30EDH fragment proofs
- 18:13Prototype tool results
- 19:17Summary
- 20:13Q&A
related talks
48mBeyond SAT - Proofs for QBF, and more
12mFO-Complete Program Verification for Heap Logics
20mAutomating Unrealizability Logic: Hoare-style Proof Synthesis for Infinite Sets of(…)
19mA Proof Recipe for Linearizability in Relaxed Memory Separation Logic
20mA Modular Approach to Metatheoretic Reasoning for Extensible Languages
16mCounterexample Driven Quantifier Instantiations with Applications to Distribute...
19mProof Automation for Linearizability in Separation Logic
05mNew foundations for probabilistic separation logic