An Introduction to Separation Logic
The work
| Authors | John C. Reynolds |
|---|---|
| Editors | |
| Type | incollection |
| 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.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-06 15:00 UTC |
Filed under
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},
isbn = {978-1-58603-976-9},
doi = {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.