Reference:

N. Rinetzky, J. Bauer, T. Reps, M. Sagiv, and R. Wilhelm. A Semantics for Procedure Local Heaps and its Abstractions. In 32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05), 2005.

Abstract:

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.

Keywords:

interprocedural, shape analysis, cutpoints

Suggested BibTeX entry:

@inproceedings{RBRSW05,
    author = {N. Rinetzky and J. Bauer and T. Reps and M. Sagiv and R. Wilhelm},
    booktitle = {32nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'05)},
    title = {{A}~{S}emantics for {P}rocedure {L}ocal {H}eaps and its {A}bstractions},
    year = {2005}
}