We present two algorithms to prove termination of programs by synthesizing linear ranking functions. The first uses an invariant generator based on iterative forward propagation with widening and extracts ranking functions from the generated invariants by manipulating polyhedral cones. It is capable of finding subtle 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 ranking functions.
In 14th International Conference on Computer Aided Verification (CAV), LNCS 2404, Springer-Verlag, pp 442-454, 2002.
Postscript, PDF. © 2001, Springer Verlag.