SA’10 Alternation for Termination
alternation termination
这篇文章结合了已有的（非）终止性证明工具以及safety checker，提出了一种新的（非）终止性证明方法。算法框架如下：
算法遍历每一个循环L，同时为其维护一个上近似O（循环不变式）和下近似U（循环中路径的子集），随后开始迭代。在每次迭代开始时，首先尝试在假设O下证明U的终止性，如果：
- 成功证明U是终止的，终止性分析工具将返回一个proof。此时验证这个proof是否适用于L，如果是，则说明L终止，考虑下一个循环；否则，返回一个反例，将其加入到U中。
- 无法证明U是终止的，但返回了一个反例（U中的一个无限路径）。此时，调用非终止性分析 工具，尝试为这个反例找到一个recurrent set 。如果成功，则用safety checker验证是否可达。如果可达，则说明程序不终止；否则，将加入到O中。
因为这一方法是基于近似的，所以可以通过已有的近似方法来处理指针、函数调用等。比如，指针的值被下近似为某个确定的变量。
因为在这一方法中用到的工具都有可能不终止，算法本身也可能不终止；此外，即使这些工具都终止，算法中的循环本身也有可能不终止。