## Practical Methods for Proving Program Termination

*Michael Colon,
Henny Sipma
*
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.

© Henny Sipma /
sipma@cs.stanford.edu
Last modified: Thu Jul 12 14:42:04 PDT 2001