Symbolic Execution with Separation Logic

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

Abstract

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.

Details

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