Interprocedural Shape Analysis with Separated Heap Abstractions

We describe an interprocedural shape analysis that makes use of spatial locality (i.e. the fact that most procedures modify only a small subset of the heap) in its representation of abstract states. Instead of tracking reachability information directly and aliasing information indirectly, our representation tracks reachability indirectly and aliasing directly. Computing the effect of procedure calls and returns on an abstract state is easy because the representation exhibits spatial locality mirroring the locality that is present in the concrete semantics. The benefits of this approach include improved speed, support for programs that deallocate memory, the handling of bounded numbers of heap cutpoints, and support for cyclic and shared data structures.

interproc.pdf
PDF file

In  Static Analysis, 13th International Symposium, SAS 2006, Seoul, Korea, August 29-31, 2006, Proceedings

Publisher  Springer

Details

TypeInproceedings
Pages240-260
Volume4134
SeriesLecture Notes in Computer Science
ISBN3-540-37756-5
> Publications > Interprocedural Shape Analysis with Separated Heap Abstractions