一句话：提出首个能精确刻画终止状态的终止条件推断方法，并证明其正确、精确、可终止且相对完备。
本文研究如何推断精确的终止条件，即所生成条件能准确刻画程序的终止状态集合。作者提出一个简洁而有效的框架：迭代识别并移除非终止状态，同时调用终止性证明器验证当前条件。该框架用数据驱动的证明器实例化，并设计多路数据共享机制以增强证明器之间的交互。论文证明该方法具备正确性、精确性、可终止性和相对完备性，并引入循环集泛化技术加速迭代收敛。基于文献程序基准的评估表明，该实现显著优于当前最先进工具 Acabar，能生成更精确的终止条件，且所提技术对加速收敛起到关键作用。
We present the first approach to infer termination conditions that are accurate in the sense of precisely characterizing terminating states. It builds on a simple but effective framework where non-terminating states are iteratively identified and removed, and a termination prover is employed to validate the current condition. We instantiate the framework with data-driven provers and design a multi-way data sharing mechanism to enhance their interaction. Our proofs show that this method is correct, accurate, terminating, and relatively complete. Additionally, we introduce generalization techniques for recurrent sets to accelerate the iteration process. Evaluation on a benchmark of programs from the literature shows that our implementation significantly outperforms the state-of-the-art tool Acabar, producing much more accurate termination conditions, with the proposed techniques playing a crucial role in speeding up the convergence of the process.