A Scalable Segmented Decision Tree Abstract Domain

Patrick Cousot 1, 2 Radhia Cousot 1, 2 Laurent Mauborgne 2, 3
2 ABSTRACTION - Abstract Interpretation and Static Analysis
DI-ENS - Département d'informatique de l'École normale supérieure, ENS Paris - École normale supérieure - Paris, Inria Paris-Rocquencourt, CNRS - Centre National de la Recherche Scientifique : UMR 8548
Abstract : The key to precision and scalability in all formal methods for static program analysis and verification is the handling of disjunctions arising in relational analyses, the flow-sensitive traversal of conditionals and loops, the context-sensitive inter-procedural calls, the interleaving of concurrent threads, etc. Explicit case enumeration immediately yields to combinatorial explosion. The art of scalable static analysis is therefore to abstract disjunctions to minimize cost while preserving weak forms of disjunctions for expressivity. Building upon packed binary decision trees to handle disjunction in tests, loops and procedure/function calls and array segmentation to handle disjunctions in array content analysis, we have introduced segmented decision trees to allow for more expressivity while mastering costs via widenings.
Type de document :
Communication dans un congrès
Z. Manna and D. Peled. Time for Verification, Essays in Memory of Amir Pnueli, Apr 2010, New York, United States. Springer-Verlag, 6200, pp.72-95, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00543632
Contributeur : Patrick Cousot <>
Soumis le : lundi 6 décembre 2010 - 14:21:56
Dernière modification le : mardi 17 avril 2018 - 11:28:55
Document(s) archivé(s) le : lundi 7 mars 2011 - 02:31:15

Fichier

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

Identifiants

  • HAL Id : inria-00543632, version 1

Collections

Citation

Patrick Cousot, Radhia Cousot, Laurent Mauborgne. A Scalable Segmented Decision Tree Abstract Domain. Z. Manna and D. Peled. Time for Verification, Essays in Memory of Amir Pnueli, Apr 2010, New York, United States. Springer-Verlag, 6200, pp.72-95, 2010, Lecture Notes in Computer Science. 〈inria-00543632〉

Partager

Métriques

Consultations de la notice

169

Téléchargements de fichiers

94