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. © Springer-Verlag Berlin Heidelberg 2001.
CITATION STYLE
Colón, M. A., & Sipma, H. B. (2001). Synthesis of linear ranking functions. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2031 LNCS, pp. 67–81). Springer Verlag. https://doi.org/10.1007/3-540-45319-9_6
Mendeley helps you to discover research relevant for your work.