Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata
Contributor : Antoine Miné Connect in order to contact the contributor
Submitted on : Tuesday, January 20, 2015 - 4:28:53 PM
Last modification on : Friday, October 15, 2021 - 1:40:29 PM


  • HAL Id : hal-01107419, version 1



Caterina Urban. FuncTion: An Abstract Domain Functor for Termination. TACAS 2015 - 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2015, Londres, United Kingdom. pp.464-466. ⟨hal-01107419⟩



Record views