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 metadatas

https://hal.inria.fr/hal-01107419
Contributor : Antoine Miné <>
Submitted on : Tuesday, January 20, 2015 - 4:28:53 PM
Last modification on : Monday, January 28, 2019 - 9:04:18 AM

Identifiers

  • HAL Id : hal-01107419, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

156