## Synthesis of Linear Ranking Functions

*Michael Colon,
Henny Sipma
*
Deductive verification of progress properties relies on finding
ranking functions to prove termination of program cycles.
We present an algorithm to synthesize linear ranking functions
that can establish such termination.
Fundamental to our approach is the representation of
systems of linear inequalities and sets of linear expressions
as polyhedral cones.
This representation allows us to reduce the search for
linear ranking functions to the computation of polars,
intersections and projections of polyhedral cones,
problems which have well-known solutions.

In *7th International Conference on Tools and Algorithms
for the Construction and Analysis of Systems (TACAS)*,
LNCS 2031, Springer-Verlag, pp 67-81, 2001.

Postscript,
PDF.
© 2001, Springer Verlag.

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