A Semantic Basis for Local Reasoning

Hongseok Yang and Peter O'Hearn

To appear at Foundations of Software Science and Computation Structures (FOSSACS02), Grenoble, France, 6-14 April, 2002


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, and thus avoided when writing specifications.

Server START Conference Manager
Update Time 14 Dec 2001 at 14:02:38
Maintainer fossacs02@brics.dk.
Start Conference Manager
Conference Systems