一句话：将命令式程序的终止性证明归约为 k-归纳不变式合成，从而更高效地合成终止性论证。
论文提出一种用 k-归纳（k-induction）证明命令式程序终止性的新方法。其核心思想是把终止性证明问题形式化为一个 k-归纳不变式合成任务。与标准的归纳方法相比，k-归纳所需的不变式更弱，因而更容易被发现；同时 k-归纳的 base case 会对程序进行展开，从而为不变式合成提供更强的前置条件。这两点结合使得终止性论证的自动合成比标准方法更高效。作者实现了该 k-归纳方法的原型工具，实验结果表明该方法在有效性与效率上都有显著提升。
We propose a novel approach to proving the termination of imperative programs by k-induction. By our approach, the termination proving problem can be formalized as a k-inductive invariant synthesis task. On the one hand, k-induction uses weaker invariants than that required by the standard inductive approach. On the other hand, the base case of k-induction, which unrolls the program, can provide stronger pre-condition for invariant synthesis. As a result, the termination arguments of our approach can be synthesized more efficiently than the standard method. We implement a prototype of our k-inductive approach. The experimental results show the significant effectiveness and efficiency of our approach.
DOI 原文 ·
@inproceedings{paperbot6018,
title = {Proving termination by
<i>k</i>
-induction},
author = {Jianhui Chen and Fei He},
booktitle = {ASE},
year = {2020},
doi = {10.1145/3324884.3418929}
}