ReFuncTion: Conditional Termination by Abstract Interpretation of Numerical C Programs (Competition Contribution)

Abstract

ReFuncTion is a static analyzer designed for proving conditional termination. The tool automatically infers piecewise-defined ranking functions and sufficient preconditions by means of abstract interpretation.

Type
Conference Paper
Publication
In Proc. 32nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026)
Date
Links
PDF Code Project HAL Springer

FuncTion