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.