Practical methods for proving program termination

Abstract

We present two algorithms to prove termination of programs by synthesizingl inear rankingf unctions. The first uses an invariant generator based on iterative forward propagation with widening and extracts rankingf unctions from the generated invariants by manipulating polyhedral cones. It is capable of findings ubtle ranking functions which are linear combinations of many program variables, but is limited to programs with few variables. The second, more heuristic, algorithm targets the class of structured programs with single-variable ranking functions. Its invariant generator uses a heuristic extrapolation operator to avoid iterative forward propagation over program loops. For the programs we have considered, this approach converges faster and the invariants it discovers are sufficiently strong to imply the existence of rankingf unctions.