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
CNRS - Centre National de la Recherche Scientifique : UMR 8548, Inria Paris-Rocquencourt, DI-ENS - Département d'informatique de l'École normale supérieure
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
Liste complète des métadonnées

Cited literature [21 references]  Display  Hide  Download

https://hal.inria.fr/hal-00760428
Contributor : Xavier Rival <>
Submitted on : Monday, December 3, 2012 - 8:30:38 PM
Last modification on : Friday, May 25, 2018 - 12:02:05 PM
Document(s) archivé(s) le : Monday, March 4, 2013 - 3:54:57 AM

File

vmcai13.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

393

Files downloads

153