A Scalable Segmented Decision Tree Abstract Domain - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2010

A Scalable Segmented Decision Tree Abstract Domain

Résumé

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.
Fichier principal
Vignette du fichier
segmentation.pdf (401.13 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00543632 , version 1 (06-12-2010)

Identifiants

  • HAL Id : inria-00543632 , version 1

Citer

Patrick Cousot, Radhia Cousot, Laurent Mauborgne. A Scalable Segmented Decision Tree Abstract Domain. Time for Verification, Essays in Memory of Amir Pnueli, Apr 2010, New York, United States. pp.72-95. ⟨inria-00543632⟩
123 Consultations
162 Téléchargements

Partager

Gmail Facebook X LinkedIn More