A Complete Method for the Synthesis of Linear Ranking Functions

by: Andreas Podelski, Andrey Rybalchenko

Verification, Model Checking, and Abstract Interpretation (2004), pp. 465-486.

View FullText article

SpringerLink

Reviews [Write a review of this article]

There are no reviews of this article

Find related articles from these CiteULike users

zuleger

Find related articles with these CiteULike tags

model_checking

Abstract

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 [PR03].

@incollection{citeulike:3042565, abstract = {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 [PR03].}, author = {Podelski, Andreas and Rybalchenko, Andrey }, citeulike-article-id = {3042565}, journal = {Verification, Model Checking, and Abstract Interpretation}, keywords = {model\_checking}, pages = {465--486}, posted-at = {2008-07-25 13:29:38}, priority = {0}, title = {A Complete Method for the Synthesis of Linear Ranking Functions}, url = {http://www.springerlink.com/content/0fc8ewqwcexp3yh9 }, year = {2004} }

RIS record

TY - CHAP ID - citeulike:3042565 L3 - citeulike-article-id:3042565 TI - A Complete Method for the Synthesis of Linear Ranking Functions JF - Verification, Model Checking, and Abstract Interpretation SP - 465 EP - 486 N2 - 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 [PR03]. KW - model_checking AU - Podelski, Andreas AU - Rybalchenko, Andrey PY - 2004/// UR - http://www.springerlink.com/content/0fc8ewqwcexp3yh9 ER -

RIS BibTeX