Implementing separation logic using an SMT-backed Frame Rule
summary
Implements an SMT-backed Frame Rule by encoding a decidable fragment of separation logic into CVC5 and integrating it into Liquid Java for symbolic execution, claiming the encoding simplifies tools like Smallfoot and GRASShopper. Provides a proof-of-concept algorithm that splits heaps in linear time over heap size, sends entailment queries to the solver, and passes lightweight benchmarks but causes a 30% compile-time increase and lacks a formal proof. Works for sequential programs and a restricted fragment; no fractional permissions and no concurrency support yet; implementation is public.
AI-written summary · about
chapters (11)
- 0:00Separation logic basics
- 2:50Liquid Java basics
- 4:17Symbolic execution
- 7:56Symbolic procedure example
- 10:23Frame rule with SMT
- 13:38Preconditions with SMT
- 15:54Limitations and benchmarks
- 18:04Benefits of the approach
- 19:09Q&A
- 20:14Extending CVC5
- 21:23Closing remarks
related talks
05mNew foundations for probabilistic separation logic
24mConcurrent Quantum Separation Logic for Fine-Grained Parallelism
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
23mVerifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach
17mCalculational design of Incorrectness Separation Logic
13mInductive Synthesis of Inductive Heap Predicates
25mA Relational Separation Logic for Effect Handlers
40mReasoning Under Uncertainty in SMT Solving, Research, and Life