A Semantic Basis for Local Reasoning
The work
| Authors | Hongseok Yang; Peter W. O'Hearn |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2002 |
| Citekey | yang2002semantic |
Where it appeared
| Published in | Foundations of Software Science and Computation Structures |
|---|---|
| Publisher | Springer |
| Series | Lecture Notes in Computer Science |
| Number in series | 2303 |
| Pages | 402--416 |
Identifiers
| DOI | 10.1007/3-540-45931-6_28 |
|---|---|
| OpenAlex | W1608869910 |
Access
| Landing page | https://doi.org/10.1007/3-540-45931-6_28 |
|---|---|
| Free full text | https://link.springer.com/content/pdf/10.1007/3-540-45931-6_28.pdf |
Related
| Distinct from | yang2001local |
|---|
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.
A copy is held
pdf, 634.7 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-26 15:20 UTC |
Filed under
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},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {402--416},
doi = {10.1007/3-540-45931-6_28},
}
This record lives at https://refs.drheap.org/yang2002semantic/ and will keep doing so.