一句话：提出组合式欠近似非终止证明逻辑 UNTer_SL，并实现可扩展分析器 Pulse∞，在数十万行代码库中发现未知非终止缺陷。
程序终止性是经典的非安全性质，其反例一般无法由有限执行迹见证，因此非终止检测难以通过测试完成。已有非终止证明工作多局限于小型自包含基准，难以应用于大型真实项目。本文提出组合式非终止证明理论：先给出 UNTer——一个可靠且完备的欠近似逻辑，用于证明非终止；再引入分离逻辑扩展为 UNTer_SL，以处理堆操作程序，并借助欠近似与双溯因（bi-abduction）实现自动化。作者基于 Meta 的 Pulse 分析器实现了自动化组合证明器 Pulse∞，在 OpenSSL、libxml2、libxpm、CryptoPP 等数十万行规模的代码库与库上运行，发现了若干此前未知的非终止缺陷并报告给相应开发者。
Program termination is a classic non-safety property whose falsification cannot in general be witnessed by a finite trace. This makes testing for non-termination challenging, and also a natural target for symbolic proof. Several works in the literature apply non-termination proving to small, self-contained benchmarks, but it has not been developed for large, real-world projects; as such, despite its allure, non-termination proving has had limited practical impact. We develop a compositional theory for non-termination proving, paving the way for its scalable application to large codebases. Discovering non-termination is an under-approximate problem, and we present UNT er , a sound and complete under-approximate logic for proving non-termination. We then extend UNT er with separation logic and develop UNTer SL for heap-manipulating programs, yielding a compositional proof method amenable to automation via under-approximation and bi-abduction. We extend the Pulse analyser from Meta and develop Pulse ∞ , an automated, compositional prover for non-termination based onx UNTer SL . We have run Pulse ∞ on large codebases and libraries, each comprising hundreds of thousands of lines of code, including OpenSSL, libxml2, libxpm and CryptoPP; we discovered several previously-unknown non-termination bugs and have reported them to developers of these libraries.