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

HAL 2026 Open access

Read full text
Authors: Naïm Moussaoui Remil, Caterina Urban
Cited by: 0

Abstract

ReFuncTion is a static analyzer designed for proving conditional termination (resilience), and functional program properties expressed in Computation Tree Logic (CTL). The tool automatically infers piecewise-defined ranking functions and sufficient preconditions by means of abstract interpretation.

Fields of Study & Subjects

Logic programming and type systems Formal Methods in Verification Software Testing and Debugging Techniques

Publication details

Journal / source
HAL
Publication date
11 April 2026
Language
EN