An Introduction to Separation Logic
The work
| Title | An Introduction to Separation Logic |
|---|---|
| Authors | John C. Reynolds |
| Type | chapter in a collection |
| Year | 2009 |
| Also known as | c2009introduction |
| Citekey | reynolds2009introduction |
Where it appeared
| Published in | Engineering Methods and Tools for Software Safety and Security |
|---|---|
| Publisher | IOS Press |
Identifiers
| DOI | 10.3233/978-1-58603-976-9-285 |
|---|---|
| OpenAlex | W4407736074 |
| ISBN | 978-1-58603-976-9 |
Access
| Landing page | https://doi.org/10.3233/978-1-58603-976-9-285 |
|---|
Abstract
Separation logic, originally developed by O'Hearn and Reynolds, is an extension of Hoare logic originally intended for reasoning about programs that use shared mutable data structures. It was based on the concept of separating conjuction, which permits the concise expression of aliasing constraints.
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-06 |
Cite it as
@incollection{reynolds2009introduction,
title = {An Introduction to Separation Logic},
author = {John C. Reynolds},
year = {2009},
booktitle = {Engineering Methods and Tools for Software Safety and Security},
publisher = {IOS Press},
doi = {10.3233/978-1-58603-976-9-285},
isbn = {978-1-58603-976-9},
url = {https://doi.org/10.3233/978-1-58603-976-9-285},
}
This record lives at https://refs.drheap.org/reynolds2009introduction/ and will keep
doing so. It used to be called c2009introduction, and those addresses still resolve to this one.