A Complete Method for the Synthesis of Linear Ranking Functions
A Complete Method for the Synthesis of Linear Ranking Functions
复制标题
DOI：
10.1007/978-3-540-24622-0_20
复制
发表时间：
2004-01
期刊：
影响因子：
--
通讯作者：
A. Podelski;A. Rybalchenko
中科院分区：
文献类型：
--
作者：
A. Podelski;A. Rybalchenko
提出了一种通过综合线性排序函数来证明非嵌套程序循环可终止性的自动化方法。该方法是完整的。也就是说，如果线性排序函数存在，那么它将被我们的方法发现。该方法依赖于这样一个事实，即我们可以获得程序循环的线性排序函数，作为我们从程序循环导出的线性不等式组的解。该方法被用作通过转移不变量证明更一般程序的终止性和其他活性性质的方法中的子例程；参见[PR03]。
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].