A Semantic Basis for Local Reasoning

The work

TitleA Semantic Basis for Local Reasoning
AuthorsHongseok Yang; Peter W. O'Hearn
Typeconference paper
Year2002
Citekeyyang2002semantic

Where it appeared

Published inFoundations of Software Science and Computation Structures
PublisherSpringer
Pages402--416

Identifiers

DOI10.1007/3-540-45931-6_28
OpenAlexW1608869910

Access

Landing pagehttps://doi.org/10.1007/3-540-45931-6_28
Free full texthttps://link.springer.com/content/pdf/10.1007/3-540-45931-6_28.pdf

Abstract

We present a semantic analysis of a recently proposed formalism for local reasoning, where a specification (and hence proof) can concentrate on only those cells that a program accesses. Our main results are the soundness and, in a sense, completeness of a rule that allows frame axioms, which describe invariant properties of portions of heap memory, to be inferred automatically; thus, these axioms can be avoided when writing specifications.

Copy held

KindPDF, 649.9 kB
Retrieved2026-08-10
Heldlocal, for personal reference
Where it came fromhttps://link.springer.com/content/pdf/10.1007/3-540-45931-6_28.pdf

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: Foundations of Software Science and Computation Structures (FoSSaCS) venue Lecture Notes in Computer Science series Separation logic topic

Cite it as

@inproceedings{yang2002semantic,
  title = {A Semantic Basis for Local Reasoning},
  author = {Hongseok Yang and Peter W. O'Hearn},
  year = {2002},
  booktitle = {Foundations of Software Science and Computation Structures},
  pages = {402--416},
  publisher = {Springer},
  doi = {10.1007/3-540-45931-6_28},
  url = {https://link.springer.com/content/pdf/10.1007/3-540-45931-6_28.pdf},
}

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