Symbolic Execution with Separation Logic

We describe a sound method for automatically proving Hoare triples for loop-free code in Separation Logic, for certain preconditions and postconditions (symbolic heaps). The method uses a form of symbolic execution, a decidable proof theory for symbolic heaps, and extraction of frame axioms from incomplete proofs. This is a precursor to the use of the logic in automatic specification checking, program analysis, and model checking.

• Type: Conference
• Year: 2005
• Where: APLAS
• Authors: Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn
• Keywords: APLAS 2005, Decidable Proof Theory, Symbolic Execution, Symbolic Heaps