Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks

Pascal Sotin 1 Xavier Rival 1, 2
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 : We propose a hierarchical shape abstract domain, so as to infer structural invariants of dynamic structures such as lists living inside static structures, such as arrays. This programming pattern is often used in safety critical embedded software that need to ''allocate'' dynamic structures inside static regions due to dynamic memory allocation being forbidden in this context. Our abstract domain precisely describes such hierarchies of structures. It combines several instances of simple shape abstract domains, dedicated to the representation of elementary shape properties, and also embeds a numerical abstract domain. This modular construction greatly simplifies the design and the implementation of the abstract domain. We provide an implementation, and show the effectiveness of our approach on a problem taken from a real code.
Type de document :
Communication dans un congrès
R. Jhala and A. Igarashi. APLAS 2012 - Asian Conference on Programming Languages And Software, Dec 2012, Kyoto, Japan. Springer, 7705, pp.131-147, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35182-2_10〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00760427
Contributeur : Xavier Rival <>
Soumis le : mardi 8 janvier 2013 - 12:03:36
Dernière modification le : vendredi 25 mai 2018 - 12:02:05
Document(s) archivé(s) le : mardi 9 avril 2013 - 03:49:12

Fichier

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

Identifiants

Collections

Citation

Pascal Sotin, Xavier Rival. Hierarchical Shape Abstraction of Dynamic Structures in Static Blocks. R. Jhala and A. Igarashi. APLAS 2012 - Asian Conference on Programming Languages And Software, Dec 2012, Kyoto, Japan. Springer, 7705, pp.131-147, 2012, Lecture Notes in Computer Science. 〈10.1007/978-3-642-35182-2_10〉. 〈hal-00760427〉

Partager

Métriques

Consultations de la notice

336

Téléchargements de fichiers

95