The Abstract Domain of Segmented Ranking Functions

Caterina Urban 1, 2, *
* Auteur correspondant
1 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
2 Abstraction
LIENS - Laboratoire d'informatique de l'école normale supérieure
Abstract : We present a parameterized abstract domain for proving program termination by abstract interpretation. The domain automatically synthesizes piecewise-defined ranking functions and infers sufficient conditions for program termination. The analysis uses over-approximations but we prove its soundness, meaning that all program executions respecting these sufficient conditions are indeed terminating. The abstract domain is parameterized by a numerical abstract domain for environments and a numerical abstract domain for functions. This parameterization allows to easily tune the trade-off between precision and cost of the analysis. We describe an instantiation of this generic do- main with intervals and affine functions. We define all abstract operators, including widening to ensure convergence. To illustrate the potential of the proposed framework, we have implemented a research prototype static analyzer, for a small imperative language, that yielded interesting preliminary results.
Type de document :
Communication dans un congrès
Logozzo, Francesco and Fähndrich, Manuel. Static Analysis, 20th International Symposium,, Jun 2013, Seattle, United States. Springer, 7935, pp.43-62, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38856-9_5〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00925670
Contributeur : Antoine Miné <>
Soumis le : mercredi 8 janvier 2014 - 14:05:08
Dernière modification le : jeudi 11 janvier 2018 - 06:26:23
Document(s) archivé(s) le : mardi 8 avril 2014 - 22:57:36

Fichier

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

Identifiants

Collections

Citation

Caterina Urban. The Abstract Domain of Segmented Ranking Functions. Logozzo, Francesco and Fähndrich, Manuel. Static Analysis, 20th International Symposium,, Jun 2013, Seattle, United States. Springer, 7935, pp.43-62, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-38856-9_5〉. 〈hal-00925670〉

Partager

Métriques

Consultations de la notice

186

Téléchargements de fichiers

225