一句话：提出首个数据驱动的 recurrent set 学习算法，可相对完备地证明程序非终止，并在公开基准上优于现有工具。
非终止性是程序验证中的基本活性性质。本文重新审视非终止性分析，提出首个用于合成 recurrent set 的数据驱动学习算法：先以一种新方法有效推测非终止样本，再通过保证收敛的学习算法，在存在有效 recurrent set 时收敛到该集合，从而建立相对完备性。作者实现原型工具，并在公开基准上评估。实验表明，该工具在证明非终止性方面优于当前最先进工具，无论求解案例数还是性能均更优；对非线性程序的评估也显示其处理复杂程序的能力。
Termination is a fundamental liveness property for program verification. In this paper, we revisit the problem of non-termination analysis and propose the first data-driven learning algorithm for synthesizing recurrent sets, where the non-terminating samples are effectively speculated by a novel method. To ensure convergence of learning, we develop a learning algorithm which is guaranteed to converge to a valid recurrent set if one exists, and thus establish its relative completeness. The methods are implemented in a prototype tool, and experimental results on public benchmarks show its efficacy in proving non-termination as it outperforms state-of-the-art tools, both in terms of cases solved and performance. Evaluation on non-linear programs also demonstrates its ability to handle complex programs.