Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Interprocedural Shape Analysis with Separated Heap Abstractions

Alexey Gotsman, Josh Berdine, and Byron Cook


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.


Publication typeInproceedings
Published inStatic Analysis, 13th International Symposium, SAS 2006, Seoul, Korea, August 29-31, 2006, Proceedings
SeriesLecture Notes in Computer Science
> Publications > Interprocedural Shape Analysis with Separated Heap Abstractions