Skip to Main content Skip to Navigation
New interface
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 - ENS Paris, 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 : Thursday, March 17, 2022 - 10:08:44 AM


  • 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