A Decision Tree Abstract Domain for Proving Conditional Termination

Caterina Urban 1 Antoine Miné 1
1 ANTIQUE - Analyse Statique par Interprétation Abstraite
DI-ENS - Département d'informatique de l'École normale supérieure, Inria Paris-Rocquencourt
Abstract : We present a new parameterized abstract domain able to refine existing numerical abstract domains with finite disjunctions. The elements of the abstract domain are decision trees where the decision nodes are labeled with linear constraints, and the leaf nodes belong to a numerical abstract domain. The abstract domain is parametric in the choice between the expressivity and the cost of the linear constraints for the decision nodes (e.g., polyhedral or octagonal constraints), and the choice of the abstract domain for the leaf nodes. We describe an instance of this domain based on piecewise-defined ranking functions for the automatic inference of sufficient preconditions for program termination. We have implemented a static analyzer for proving conditional termination of programs written in (a subset of) C and, using experimental evidence, we show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art and is able to analyze programs that are out of the reach of existing methods.
Type de document :
Communication dans un congrès
21st International Static Analysis Symposium (SAS'14), Sep 2014, Munich, Germany. Springer, 8373, pp.17, 2014, Lecture Notes in Computer Science. 〈http://cs.uni-muenster.de/sev/sas14/〉. 〈10.1007/978-3-319-10936-7_19〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01105221
Contributeur : Antoine Miné <>
Soumis le : mardi 20 janvier 2015 - 15:40:59
Dernière modification le : jeudi 11 janvier 2018 - 02:02:37
Document(s) archivé(s) le : mardi 21 avril 2015 - 10:11:25

Fichier

article-urban-mine-sas14.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Caterina Urban, Antoine Miné. A Decision Tree Abstract Domain for Proving Conditional Termination. 21st International Static Analysis Symposium (SAS'14), Sep 2014, Munich, Germany. Springer, 8373, pp.17, 2014, Lecture Notes in Computer Science. 〈http://cs.uni-muenster.de/sev/sas14/〉. 〈10.1007/978-3-319-10936-7_19〉. 〈hal-01105221〉

Partager

Métriques

Consultations de la notice

330

Téléchargements de fichiers

140