A complete method for the synthesis of linear ranking functions. (English) Zbl 1202.68109
Steffen, Bernhard (ed.) et al., Verification, model checking, and abstract interpretation. 5th international conference, VMCAI 2004, Venice, Italy, January 11–13, 2004. Proceedings. Berlin: Springer (ISBN 3-540-20803-8/pbk). Lect. Notes Comput. Sci. 2937, 239-251 (2004).
Summary: We present an automated method for proving the termination of an unnested program loop by synthesizing linear ranking functions. The method is complete. Namely, if a linear ranking function exists then it will be discovered by our method. The method relies on the fact that we can obtain the linear ranking functions of the program loop as the solutions of a system of linear inequalities that we derive from the program loop. The method is used as a subroutine in a method for proving termination and other liveness properties of more general programs via transition invariants; see [A. Podelski and A. Rybalchenko, Software model checking of liveness properties via transition invariants. MPI Technical Report 2-004, available at http://www.mpi-sws.org/~rybal/papers/MPI-I-2003-2-004.liveness-via-transition-invariants.pdf (2003)].
For the entire collection see [Zbl 1031.68005].
For the entire collection see [Zbl 1031.68005].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
