一句话：提出数据驱动的循环界学习方法，结合学习器与验证检查器，高效证明程序终止性。
终止性是程序验证中的基本活性性质，而循环界给出了循环迭代次数的上界，其存在即可证明程序终止。本文提出一种强化的黑盒学习式终止性证明框架，由循环界学习器与验证检查器两部分组成。作者给出高效的数据驱动算法，可推断多种循环界，包括简单循环界、合取式循环界与字典序循环界；同时设计了集成快速界检查算法与双向数据共享机制的高效验证检查器。原型工具 ddlTerm 在公开基准上进行了实验评估，结果表明其相比当前最先进的终止性分析工具能多求解 13%–48% 的基准，并节省 40%–77% 的求解时间。
Termination is a fundamental liveness property for program verification. A loop bound is an upper bound of the number of loop iterations for a given program. The existence of a loop bound evidences the termination of the program. This paper employs a reinforced black-box learning approach for termination proving, consisting of a loop bound learner and a validation checker. We present efficient data-driven algorithms for inferring various kinds of loop bounds, including simple loop bounds, conjunctive loop bounds, and lexicographic loop bounds. We also devise an efficient validation checker by integrating a quick bound checking algorithm and a two-way data sharing mechanism. We implemented a prototype tool called ddlTerm. Experiments on publicly accessible benchmarks show that ddlTerm outperforms state-of-the-art termination analysis tools by solving 13-48% more benchmarks and saving 40--77% solving time.