Abstract

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.