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.
https://hal.inria.fr/hal-01107419
Contributor : Antoine Miné <>
Submitted on : Tuesday, January 20, 2015 - 4:28:53 PM Last modification on : Tuesday, September 22, 2020 - 3:51:33 AM
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⟩