Symbolic Execution with Separation Logic
The work
| Authors | Josh Berdine; Cristiano Calcagno; Peter W. O'Hearn |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2005 |
| Citekey | berdine2005symbolic |
Where it appeared
| Published in | Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 3780 |
| Volume | 3780 |
| Pages | 52--68 |
Identifiers
| DOI | 10.1007/11575467_5 |
|---|
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.
A copy is held
pdf, 499.9 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-18 16:22 UTC |
Filed under
Cite it as
@inproceedings{berdine2005symbolic,
title = {Symbolic Execution with Separation Logic},
author = {Josh Berdine and Cristiano Calcagno and Peter W. O'Hearn},
year = {2005},
booktitle = {Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {3780},
pages = {52--68},
doi = {10.1007/11575467_5},
}
This record lives at https://refs.drheap.org/berdine2005symbolic/ and will keep doing so.