Region-based shape analysis with tracked locations

12 years 5 months ago
Region-based shape analysis with tracked locations
This paper proposes a novel approach to shape analysis: using local reasoning about individual heap locations of global reasoning about entire heap abstractions. We present an inter-procedural shape analysis algorithm for languages with destructive updates and formulate it as a dataflow analysis. The key feature is a novel memory ion that differs from traditional abstractions in two ways. First, we build the shape abstraction and analysis on pointer analysis. Second, we decompose the shape abstraction into a set of independent configurations, each of which characterizes one single heap location. Our approach: 1) leads to simpler algorithm specifications, because reasoning about the single location; 2) leads to efficient algorithms, because of the abstraction decomposition; and 3) makes it easier to develop context-sensitive, demand-driven, and incremental shape analyses. We have developed simple extensions that use the analysis results to find memory errors in programs with explicit d...
Brian Hackett, Radu Rugina
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where POPL
Authors Brian Hackett, Radu Rugina
Comments (0)