Non-Termination Proving: 100 Million LoC and Beyond
作者: Julien Vanegue, Jules Villard, Peter O'Hearn, Azalea Raad
分类: cs.PL, cs.CL, cs.SE
发布日期: 2025-09-05
备注: 14 pages, 4 figures
💡 一句话要点
Pulse Infinite：利用证明技术检测大型程序中的非终止问题
🎯 匹配领域: 支柱八：物理动画 (Physics-based Animation)
关键词: 非终止性检测 程序验证 组合式分析 欠近似 大规模代码 软件质量保证 静态分析
📋 核心要点
- 现有非终止性检测方法难以扩展到大型代码库，无法满足实际工业需求。
- Pulse Infinite采用组合式和欠近似方法，在保证可靠性的前提下，实现了对大规模代码的分析。
- Pulse Infinite成功应用于超过一亿行代码的真实项目，发现了30多个先前未知的非终止问题。
📝 摘要（中文）
本文介绍了Pulse Infinite，一个使用证明技术来展示大型程序中非终止性（发散）的工具。Pulse Infinite以组合式和欠近似的方式工作：前者支持规模化，后者确保了证明发散的可靠性。先前的工作主要集中在几十或几百行代码（LoC）的小型基准测试上，其规模限制了它们的实用性：单个公司可能拥有数千万甚至数亿行或更多的代码。本文报告了将Pulse Infinite应用于超过一亿行用C、C++和Hack编写的开源和专有软件，识别出超过30个以前未知的非终止问题，为检测真实代码库中的发散问题建立了新的技术水平。
🔬 方法详解
问题定义：论文旨在解决大型程序中难以检测的非终止性（发散）问题。现有方法，如基于符号执行或模型检测的技术，在处理大型代码库时面临着状态空间爆炸的挑战，难以扩展到实际工业规模的应用。因此，如何高效且可靠地检测大型程序中的非终止性成为了一个关键问题。
核心思路：Pulse Infinite的核心思路是采用组合式和欠近似的方法。组合式分析允许将大型程序分解为更小的模块进行分析，从而降低了复杂性。欠近似保证了如果Pulse Infinite报告了非终止性，那么该程序确实会发散，从而保证了结果的可靠性。这种方法牺牲了完整性（可能漏报一些非终止性），但换取了在大规模代码上的可扩展性和可靠性。
技术框架：Pulse Infinite的整体框架包含以下几个主要阶段：首先，程序被分解为多个模块。然后，对每个模块进行独立的分析，以推断其可能的状态转换。接下来，使用欠近似技术来抽象这些状态转换，并构建一个抽象模型。最后，使用证明技术来验证该抽象模型是否存在无限循环，从而证明程序的非终止性。
关键创新：Pulse Infinite的关键创新在于其组合式和欠近似的结合。传统的非终止性检测方法往往难以同时保证可扩展性和可靠性。Pulse Infinite通过组合式分析实现了可扩展性，并通过欠近似保证了可靠性。这种结合使得Pulse Infinite能够有效地处理大规模代码库。
关键设计：Pulse Infinite的具体技术细节包括：使用分离逻辑（Separation Logic）来形式化程序的语义；采用符号执行和抽象解释相结合的方法来推断程序的状态转换；使用归纳推理来证明抽象模型中的无限循环。此外，Pulse Infinite还包含一些启发式规则，用于优化分析过程，提高效率。
🖼️ 关键图片
📊 实验亮点
Pulse Infinite成功应用于超过一亿行代码的开源和专有软件，发现了30多个以前未知的非终止问题。这些问题涵盖了C、C++和Hack等多种编程语言，证明了Pulse Infinite的广泛适用性。实验结果表明，Pulse Infinite在检测大规模代码库中的非终止性问题方面，达到了新的技术水平。
🎯 应用场景
该研究成果可应用于软件质量保证、安全漏洞检测等领域。通过自动检测程序中的非终止性问题，可以帮助开发者尽早发现和修复潜在的缺陷，提高软件的可靠性和安全性。尤其在大型软件项目中，该技术能够显著降低人工代码审查的成本，并提高问题发现的效率。未来，该技术有望集成到CI/CD流程中，实现持续的非终止性检测。
📄 摘要（原文）
We report on our tool, Pulse Infinite, that uses proof techniques to show non-termination (divergence) in large programs. Pulse Infinite works compositionally and under-approximately: the former supports scale, and the latter ensures soundness for proving divergence. Prior work focused on small benchmarks in the tens or hundreds of lines of code (LoC), and scale limits their practicality: a single company may have tens of millions, or even hundreds of millions of LoC or more. We report on applying Pulse Infinite to over a hundred million lines of open-source and proprietary software written in C, C++, and Hack, identifying over 30 previously unknown issues, establishing a new state of the art for detecting divergence in real-world codebases.