Calculational design of Incorrectness Separation Logic
summary
A semantics-first proof recipe called calculational design derives axioms from closure operators (frame, disjunction, consequence) and picks minimal elements to form a parametric, sound-and-complete under-approximation proof system. Instantiated with ISL and a concurrent ISL model, it produces more derivable triples than ISL (example: start with x = x' then frame x' = 5 then ∃x' yields a triple not derivable in ISL) by using a frame rule restricted to auxiliary variables and assuming an infinite supply of auxiliary variables.
AI-written summary · about
chapters (12)
- 0:00Incorrectness separation logic intro
- 0:23Traditional proof system problems
- 1:06Calculation design approach
- 2:10Contributions to program logic
- 3:13Under-approximation separation logic
- 5:02Closure operators in under-approximation
- 7:33Minimal elements and frame rules
- 8:55Semantic proof system for ISL
- 10:02Concurrent ISL completeness
- 12:35Extending to concurrent semantics
- 14:01Future work and applications
- 14:47Q&A
related talks
21mOutcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…)
29mSynthesizing Axiomatizations using Logic Learning
22mImplementing separation logic using an SMT-backed Frame Rule
18mCertified Semantics for Disequality
14mLOUD: Synthesizing Strongest and Weakest Specifications
25mA Logic for the Imprecision of Abstract Interpretations
32mA mechanised and constructive reverse analysis of soundness and completeness of b...
13mInductive Synthesis of Inductive Heap Predicates