Shape Analysis by Graph Decomposition
R. Manevich1
, J. Berdine3
, B. Cook3
, G. Ramalingam2
and M. Sagiv1 
| (2) |
Microsoft Research, India |
| (3) |
Microsoft Research Cambridge, |
Abstract
Programs commonly maintain multiple linked data structures. Correlations between multiple data structures may often be non-existent or irrelevant to verifying that the program satisfies certain safety properties or invariants. In this paper, we show how this independence between different (singly-linked) data structures can be utilized to perform shape analysis and verification more efficiently.
We present a new abstraction based on decomposing graphs into sets of subgraphs, and show that, in practice, this new abstraction
leads to very little loss of precision, while yielding substantial improvements to efficiency.
References secured to subscribers.