Shape Analysis by Graph Decomposition

Roman Manevich, Josh Berdine, Byron Cook, Ganesan Ramalingam, and Mooly Sagiv


Programs commonly maintain multiple linked data structures. Correlations between multiple data structures may often be nonexistent 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.


Publication typeInproceedings
Published inTools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007 Braga, Portugal, March 24 - April 1, 2007, Proceedings
SeriesLecture Notes in Computer Science
PublisherSpringer Verlag
> Publications > Shape Analysis by Graph Decomposition