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.
Type de document :
Communication dans un congrès
Roberto Giacobazzi and Josh Berdine and Isabella Mastroeni. VMCAI 2013 : 14th International Conference on Verification, Model Checking and Abstract Interpretation, Jan 2013, Rome, Italy. Springer, 7737, pp.375-395, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35873-9_23〉
Liste complète des métadonnées

Littérature citée [21 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00760428
Contributeur : Xavier Rival <>
Soumis le : lundi 3 décembre 2012 - 20:30:38
Dernière modification le : mardi 24 avril 2018 - 17:20:13
Document(s) archivé(s) le : lundi 4 mars 2013 - 03:54:57

Fichier

vmcai13.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Antoine Toubhans, Bor-Yuh Evan Chang, Xavier Rival. Reduced Product Combination of Abstract Domains for Shapes. Roberto Giacobazzi and Josh Berdine and Isabella Mastroeni. VMCAI 2013 : 14th International Conference on Verification, Model Checking and Abstract Interpretation, Jan 2013, Rome, Italy. Springer, 7737, pp.375-395, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35873-9_23〉. 〈hal-00760428〉

Partager

Métriques

Consultations de la notice

307

Téléchargements de fichiers

131