Componentized heap abstraction

In this paper we present a new heap abstraction that seeks to strike a balance between the use of non-local (transitive) properties to gain precision and exploiting heap-locality. The abstraction represents the heap as an (evolving) tree of heapcomponents, with only a single heap-component being accessible at any time. The representation is tailored to yield several benefits: (a) It localizes the effect of heap mutation, enabling more efficient processing of heap mutations; (b) The representation is more space-efficient as it permits heap-components with isomorphic contents to use a shared representation; (c) It enables a more precise identification of the “input heap” to a procedure, increasing the reuse of summaries in a tabulationbased interprocedural analysis, making it more efficient. Furthermore, based on our new abstraction, an analysis can compute parameterized summaries which can be re-used for analyzing clients of instantiations of the generic data-structures.