Shape Analysis by Graph Decomposition

Abstract. 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 ion based on decomposing graphs into sets of subgraphs, and t, in practice, this new abstraction leads to very little loss of precision, while yielding substantial improvements to efficiency.

• Type: Conference
• Year: 2007
• Where: TACAS
• Authors: Roman Manevich, Josh Berdine, Byron Cook, G. Ramalingam, Mooly Sagiv
• Keywords: Algorithms, Data Structures, Multiple Data Structures, Multiple Linked Data, TACAS 2007