FuncTion
FuncTion: An Abstract Domain Functor for Termination. 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.
References in zbMATH (referenced in 2 articles )
Showing results 1 to 2 of 2.
Sorted by year (- Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
- D’Silva, Vijay; Urban, Caterina: Conflict-driven conditional termination (2015)