Piecewise-Defined Ranking Functions

Caterina Urban

Abstract

We present the design and implementation of an abstract domain for proving program termination by abstract interpretation. The domain automatically synthesizes piecewise-defined ranking functions and infers sufficient conditions for program termination. The analysis is sound, meaning that all program executions respecting these sufficient conditions are indeed terminating. We discuss the limitations of the proposed framework, and we investigate possible future work. In particular, we explore potential extensions of the abstract domain considering piecewise-defined non-linear ranking functions such as polynomials or exponentials.