Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Nikolaj S. Bjørner, Anca Browne, Eddie S. Chang, Michael Colón, Arjun Kapur, Zohar Manna, Henny B. Sipma, and Tomá s E. Uribe. STeP: The Stanford Temporal Prover, User’s Manual. Technical Report STAN-CS-TR-95-1562, Computer Science Department, Stanford University, 1995.
Nikolaj S. Bjårner, Anca Browne, and Zohar Manna. Automatic generation of invariants and intermediate assertions. Theoretical Computer Science, 173(1):49–87, 1997.
Saddek Bensalem, Yassine Lakhnech, and Hassen Saidi. Powerful techniques for the automatic generation of invariants. In Rajeev Alur and Thomas A. Henzinger, editors, CAV’96, volume 1102 of LNCS, pages 323–335. Springer-Verlag, 1996.
Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In 4th A.C.M. Symposium on Principles of Programming Languages, 1977.
Joanne R. Collier, Nicholas A.M. Monk, Philip K. Maini, and Julian H. Lewis. Pattern formation by lateral inhibition with feedback: a mathematical model of delta-notch intercellular signalling. J. Theoretical. Biology, 183:429–446, 1996.
Dennis Dams, Rob Gerth, and Orna Grumberg. A heuristic for the automatic generation of ranking functions. In Workshop on Advances in Verification (WAVe’00), pages 1–8, 2000.
David Dill. personal communication. August 2000.
Komei Fukuda and Alain Prodon. Double description method revisited. In Combinatorics and Computer Science. 1996.
David Gale. The Theory of Linear Economic Models. McGraw Hill, 1960.
Steven M. German and B. Wegbreit. A Synthesizer of Inductive Assertions. IEEE transactions on Software Engineering, 1(1):68–75, March 1975.
Shmuel Katz and Zohar Manna. Logical analysis of programs. Communications of the ACM, 19(4):188–206, April 1976.
H. W. Kuhn. Solvability and consistency for linear equations and inequalities. American Mathematics Monthly, 63, 1956.
P. McMullen. The maximum numbers of faces of a convex polytope. Mathematika, 17(4):179–184, 1970.
Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.
T.S. Motzkin, H. Raiffa, G. L. Thompson, and R. M. Thrall. The double description method. In H. W. Kuhn and A. W. Tucker, editors, Contributions to the Theory of Games II. Princeton University Press, 1953.
Gosh Ronojoy and Claire Tomlin. Lateral inhibition through delta-notch signaling. a piecewise affine hybrid model. Technical report, Stanford University, 2000.
Alexander Schrijver. Theory of Linear and Integer Programming. Wiley, 1986.
J. Telgen. Minimal representation of convex polyhedral sets. Journal of Optimization Theory and Application, 38:1–24, 1982.
Doran K. Wilde. A library for doing polyhedral operations. Technical report, IRISA, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Colóon, M.A., Sipma, H.B. (2001). Synthesis of Linear Ranking Functions. In: Margaria, T., Yi, W. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001. Lecture Notes in Computer Science, vol 2031. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45319-9_6
Download citation
DOI: https://doi.org/10.1007/3-540-45319-9_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41865-8
Online ISBN: 978-3-540-45319-2
eBook Packages: Springer Book Archive