An Overview of Separation Logic

The work

TitleAn Overview of Separation Logic
AuthorsJohn Reynolds
Typeconference paper
Year2008
Citekeyreynolds2008overview

Where it appeared

Published inVerified Software: Theories, Tools, Experiments
PublisherSpringer
Pages460--469

Identifiers

DOI10.1007/978-3-540-69149-5_49
OpenAlexW1603300426

Access

Landing pagehttps://doi.org/10.1007/978-3-540-69149-5_49
Free full texthttps://link.springer.com/content/pdf/10.1007/978-3-540-69149-5_49.pdf

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.

Copy held

KindPDF, 411.8 kB
Retrieved2026-08-10
Heldlocal, for personal reference
Where it came fromhttps://link.springer.com/content/pdf/10.1007/978-3-540-69149-5_49.pdf?error=cookies_not_supported&code=e4f2b3c1-2bdd-4c6e-adff-58bc4fe1f7b8

Where this came from

How it got herethe agent went looking · found via openalex
First seen2026-08-04
Recordreviewed by a person
Approved2026-08-16
In: Lecture Notes in Computer Science series Separation logic topic Verified Software: Theories, Tools, Experiments (VSTTE) venue

Cite it as

@inproceedings{reynolds2008overview,
  title = {An Overview of Separation Logic},
  author = {John Reynolds},
  year = {2008},
  booktitle = {Verified Software: Theories, Tools, Experiments},
  pages = {460--469},
  publisher = {Springer},
  doi = {10.1007/978-3-540-69149-5_49},
  url = {https://link.springer.com/content/pdf/10.1007/978-3-540-69149-5_49.pdf},
}

This record lives at https://refs.drheap.org/reynolds2008overview/ and will keep doing so.