FuncTion: An Abstract Domain Functor for Termination

Caterina Urban 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 : FuncTion is a research prototype static analyzer designed for proving (conditional) termination of C programs. The tool automatically infers piecewise-defined ranking functions (and sufficient preconditions for termination) by means of abstract interpretation. It combines a variety of abstract domains in order to balance the precision and cost of the analysis.
Type de document :
Communication dans un congrès
Christel Baier; Cesare Tinelli. TACAS 2015 - 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2015, Londres, United Kingdom. Springer, pp.464-466, Lecture Notes in Computer Science. 〈http://www.etaps.org/2015/tacas〉
Liste complète des métadonnées
https://hal.inria.fr/hal-01107419
Contributeur : Antoine Miné <>
Soumis le : mardi 20 janvier 2015 - 16:28:53
Dernière modification le : lundi 28 janvier 2019 - 09:04:18

Identifiants

  • HAL Id : hal-01107419, version 1

Collections

INRIA | PSL | ENS-PARIS | INRIA-ROCQ

Citation

Caterina Urban. FuncTion: An Abstract Domain Functor for Termination. Christel Baier; Cesare Tinelli. TACAS 2015 - 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2015, Londres, United Kingdom. Springer, pp.464-466, Lecture Notes in Computer Science. 〈http://www.etaps.org/2015/tacas〉. 〈hal-01107419〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

127

Contact


archive-ouverte@inria.fr