The Abstract Domain of Piecewise-Defined Ranking Functions

Abstract

We present a parameterized 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 uses over-approximations but we prove its soundness, meaning that all program executions respecting these sufficient conditions are indeed terminating. The abstract domain is parametric in the choices of the state abstraction, used for partitioning the program states, and the type of functions used as ranking functions. This parameterization allows to easily tune the trade-off between precision and cost of the analysis. We describe an instance of the abstract domain based on intervals and affine functions. We also propose an extension of the abstract domain to ordinal-valued ranking function. To illustrate the potential of the proposed framework, we have implemented a research prototype static analyzer, for a small while-language, that yielded interesting preliminary results. In particular, we are able to successfully analyze small but intricate examples that are out of the reach of existing methods.