An Overview of Separation Logic
The work
| Authors | John Reynolds |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2008 |
| Citekey | reynolds2008overview |
Where it appeared
| Published in | Verified Software: Theories, Tools, Experiments |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 4171 |
| Pages | 460--469 |
Identifiers
| DOI | 10.1007/978-3-540-69149-5_49 |
|---|---|
| OpenAlex | W1603300426 |
Access
| Landing page | https://doi.org/10.1007/978-3-540-69149-5_49 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007/978-3-540-69149-5_49.pdf |
Related
| Distinct from | ohearn2012primer |
|---|---|
| Distinct from | reynolds2002separation |
| Distinct from | reynolds2009introduction |
Abstract
After some general remarks about program verification, we introduce separation logic, a novel extension of Hoare logic that can strengthen the applicability and scalability of program verification for imperative programs that use shared mutable data structures or shared-memory concurrency.
A copy is held
pdf, 402.2 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-08-04 00:00 UTC |
| Approved by | a person 2026-08-24 14:55 UTC |
Filed under
Cite it as
@inproceedings{reynolds2008overview,
title = {An Overview of Separation Logic},
author = {John Reynolds},
year = {2008},
booktitle = {Verified Software: Theories, Tools, Experiments},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {460--469},
doi = {10.1007/978-3-540-69149-5_49},
}
This record lives at https://refs.drheap.org/reynolds2008overview/ and will keep doing so.