ReFuncTion: Conditional Termination by Abstract Interpretation of Numerical C Programs
摘要
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.