Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Symbolic Execution with Separation Logic

Josh Berdine, Cristiano Calcagno, and Peter W. O'Hearn


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.


Publication typeInproceedings
Published inProgramming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings
SeriesLecture Notes in Computer Science
> Publications > Symbolic Execution with Separation Logic