Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

11

APLAS
2005
ACM

favoriteEmaildiscussreport

116views Programming Languages» more APLAS 2005»

Symbolic Execution with Separation Logic

13 years 10 months ago

Symbolic Execution with Separation Logic

Download research.microsoft.com

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 speciﬁcation checking, program analysis, and model checking.

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

Real-time Traffic

APLAS 2005 | Decidable Proof Theory | Symbolic Execution | Symbolic Heaps |

claim paper

Related Content

» Cyclic proofs of program termination in separation logic

» Verifying Executable ObjectOriented Specifications with Separation Logic

» Compositional Proofs with Symbolic Execution

» Exploiting program dependencies for scalable multiplepath symbolic execution

» Interactive verification of concurrent systems using symbolic execution

» A Method for Implementing Equational Theories as Logic Programs

» Inferring Invariants by Symbolic Execution

» Dynamic Symbolic Execution for Testing Distributed Objects

» Database state generation via dynamic symbolic execution for coverage criteria

Post Info
More Details (n/a)

Added	26 Jun 2010
Updated	26 Jun 2010
Type	Conference
Year	2005
Where	APLAS
Authors	Josh Berdine, Cristiano Calcagno, Peter W. O'Hearn

Comments (0)