Separation logic: a logic for shared mutable data structures
The work
| Title | Separation logic: a logic for shared mutable data structures |
|---|---|
| Authors | John C. Reynolds |
| Type | conference paper |
| Year | 2002 |
| Also known as | reynolds2003separation |
| Citekey | reynolds2002separation |
Where it appeared
| Published in | Proceedings 17th Annual IEEE Symposium on Logic in Computer Science |
|---|---|
| Publisher | IEEE |
| Pages | 55--74 |
Identifiers
| DOI | 10.1109/lics.2002.1029817 |
|---|---|
| OpenAlex | W2137628566 |
Access
| Landing page | https://doi.org/10.1109/lics.2002.1029817 |
|---|
Abstract
In joint work with Peter O'Hearn and others, based on early ideas of Burstall, we have developed an extension of Hoare logic that permits reasoning about low-level imperative programs that use shared mutable data structure. The simple imperative programming language is extended with commands (not expressions) for accessing and modifying shared structures, and for explicit allocation and deallocation of storage. Assertions are extended by introducing a "separating conjunction" that asserts that its subformulas hold for disjoint parts of the heap, and a closely related "separating implication". Coupled with the inductive definition of predicates on abstract data structures, this extension permits the concise and flexible description of structures with controlled sharing. In this paper, we survey the current development of this program logic, including extensions that permit unrestricted address arithmetic, dynamically allocated arrays, and recursive procedures. We also discuss promising future directions.
Where this came from
| How it got here | the agent went looking · found via openalex |
|---|---|
| First seen | 2026-08-04 |
| Standing | endorsed |
| Approved | 2026-08-07 |
Cite it as
@inproceedings{reynolds2002separation,
title = {Separation logic: a logic for shared mutable data structures},
author = {John C. Reynolds},
year = {2002},
booktitle = {Proceedings 17th Annual IEEE Symposium on Logic in Computer Science},
pages = {55--74},
publisher = {IEEE},
doi = {10.1109/lics.2002.1029817},
url = {https://doi.org/10.1109/lics.2002.1029817},
}
This record lives at https://refs.drheap.org/reynolds2002separation/ and will keep
doing so. It used to be called reynolds2003separation, and those addresses still resolve to this one.