An Abstract Domain Combinator for Separately Conjoining Memory Abstractions - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2014

An Abstract Domain Combinator for Separately Conjoining Memory Abstractions

Résumé

The breadth and depth of heap properties that can be inferred by theunion of today’s shape analyses is quite astounding. Yet, achieving scalabilitywhile supporting a wide range of complex data structures in a generic way remainsa long-standing challenge. In this paper, we propose a way to side-stepthis issue by defining a generic abstract domain combinator for combining memoryabstractions on disjoint regions. In essence, our abstract domain constructionis to the separating conjunction in separation logic as the reduced product constructionis to classical, non-separating conjunction. This approach eases the designof the analysis as memory abstract domains can be re-used by applying ourseparating conjunction domain combinator. And more importantly, this combinatorenables an analysis designer to easily create a combined domain that appliescomputationally-expensive abstract domains only where it is required.
Fichier principal
Vignette du fichier
SAS14.pdf (247.17 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01095934 , version 1 (16-12-2014)

Identifiants

Citer

Antoine Toubhans, Bor-Yuh Evan Chang, Xavier Rival. An Abstract Domain Combinator for Separately Conjoining Memory Abstractions. Static Analysis Symposium, Sep 2014, München, Germany. ⟨10.1007/978-3-319-10936-7_18⟩. ⟨hal-01095934⟩
160 Consultations
113 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More