FuncTion: An Abstract Domain Functor for Termination (Competition Contribution)

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.

Publication
In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015)
Date

FuncTion