Counterexample-Guided Inference of Ranking Functions


Proving program termination is essential to ensure total correctness of programs. In this work, we combine recent advances in Abstract Interpretation and Software Model Checking and we propose a new method for proving termination and non-termination of programs. Inspired by recent work on the inference of ranking functions by abstract interpretation, we infer lexicographic ranking functions which over-approximate the number of loop iterations needed for termination. We incrementally refine a termination argument according to counterexamples produced by an SMT-based model checking engine. We also introduce max expressions in order to incorporate disjunctive reasoning.

To illustrate the potential of the proposed method, we have implemented a prototype analyzer that yielded interesting preliminary results. The approach has potential for future extensions for providing richer information as timing bounds, and for proving other liveness properties.

🇺🇸 SRI International, USA