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.

Type
Conference Paper
Publication
In Proc. 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015)
Acceptance: 27.4%
Date
Links
PDF Code Project BibTeX HAL Springer FuncTion

FuncTion