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.
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⟩