A Semantics for Procedure Local Heaps and its Abstractions
N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm
The goal of this work is to develop compile-time algorithms for
automatically verifying properties of imperative programs that
manipulate dynamically allocated storage. The paper presents an
analysis method that uses a characterization of a procedure's
behavior in which parts of the heap not relevant to the procedure
are ignored. The paper has two main parts:
The first part introduces a non-standard concrete semantics,
LSL, in which called procedures are only passed parts of
the heap. In this semantics, objects are treated specially when
they
separate the ``local heap'' that can be mutated by a procedure
from the rest of the heap, which---from the viewpoint of that
procedure---is non-accessible and immutable.
The second part concerns abstract interpretation of LSL and
develops a new static-analysis algorithm using canonical
abstraction.
(Click here to access the paper:
PDF.)