Skip to Main content Skip to Navigation
Conference papers

Reduced Product Combination of Abstract Domains for Shapes

Antoine Toubhans 1 Bor-Yuh Evan Chang 2 Xavier Rival 1, 3
1 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : Real-world data structures are often enhanced with additional pointers capturing alternative paths through a basic inductive skeleton (e.g., back pointers, head pointers). From the static analysis point of view, we must obtain several interlocking shape invariants. At the same time, it is well understood in abstract interpretation design that supporting a separation of concerns is critically important to designing powerful static analyses. Such a separation of concerns is often obtained via a reduced product on a case-by-case basis. In this paper, we lift this idea to abstract domains for shape analyses, introducing a domain combination operator for memory abstractions. As an example, we present simultaneous separating shape graphs, a product construction that combines instances of separation logic-based shape domains. The key enabler for this construction is a static analysis on inductive data structure definitions to derive relations between the skeleton and the alternative paths. From the engineering standpoint, this construction allows each component to reason independently about different aspects of the data structure invariant and then separately exchange information via a reduction operator. From the usability standpoint, we enable describing a data structure invariant in terms of several inductive definitions that hold simultaneously.
Document type :
Conference papers
Complete list of metadata

Cited literature [21 references]  Display  Hide  Download
Contributor : Xavier Rival <>
Submitted on : Monday, December 3, 2012 - 8:30:38 PM
Last modification on : Thursday, July 1, 2021 - 5:58:03 PM
Long-term archiving on: : Monday, March 4, 2013 - 3:54:57 AM


Files produced by the author(s)




Antoine Toubhans, Bor-Yuh Evan Chang, Xavier Rival. Reduced Product Combination of Abstract Domains for Shapes. VMCAI 2013 : 14th International Conference on Verification, Model Checking and Abstract Interpretation, Jan 2013, Rome, Italy. pp.375-395, ⟨10.1007/978-3-642-35873-9_23⟩. ⟨hal-00760428⟩



Record views


Files downloads