Non-Termination Proving: 100 Million LoC and Beyond

📄 arXiv: 2509.05293v1 📥 PDF

作者: 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)

关键词: 非终止性检测 程序验证 分离逻辑 组合式分析 欠近似 大规模代码 软件质量保证

📋 核心要点

  1. 现有非终止性检测方法难以扩展到大型代码库，无法满足实际工业需求。
  2. Pulse Infinite采用组合式和欠近似方法，在保证可靠性的前提下，支持大规模代码的分析。
  3. 实验表明，Pulse Infinite在超过一亿行代码的真实项目中发现了30多个未知的非终止问题。

📝 摘要（中文）

本文介绍了一种名为Pulse Infinite的工具，它使用证明技术来展示大型程序中的非终止性（发散）。Pulse Infinite以组合式和欠近似的方式工作：前者支持规模化，后者确保了证明发散的可靠性。先前的工作主要集中在几十或几百行代码（LoC）的小型基准测试上，其规模限制了它们的实用性：单个公司可能拥有数千万甚至数亿行或更多的代码。我们报告了将Pulse Infinite应用于超过一亿行用C、C++和Hack编写的开源和专有软件的实验结果，识别了超过30个以前未知的非终止问题，为检测真实代码库中的发散问题建立了新的技术水平。

🔬 方法详解

问题定义：论文旨在解决大型程序中难以检测的非终止（发散）问题。现有方法，如基于符号执行或抽象解释的技术，在处理大规模代码时面临着巨大的计算复杂度和状态空间爆炸问题，导致无法有效地检测出程序中的无限循环或递归等非终止行为。这些方法通常只能处理几十或几百行代码，难以应用于实际的工业级代码库。

核心思路：Pulse Infinite的核心思路是采用组合式和欠近似的方法来解决大规模代码的非终止性检测问题。组合式方法允许将程序分解为更小的模块进行分析，从而降低了计算复杂度。欠近似方法则保证了检测结果的可靠性，即如果Pulse Infinite报告了非终止性，那么程序确实存在非终止行为。

技术框架：Pulse Infinite的整体框架包含以下几个主要阶段：1) 程序解析和转换：将C、C++或Hack代码解析为中间表示形式。2) 组合式分析：将程序分解为更小的模块，并对每个模块进行独立的分析。3) 欠近似证明：使用逻辑推理和证明技术来验证每个模块是否存在非终止行为。4) 结果汇总：将各个模块的分析结果进行汇总，并报告整个程序的非终止性检测结果。

关键创新：Pulse Infinite的关键创新在于其组合式和欠近似的分析方法。与传统的整体分析方法相比，组合式方法能够显著降低计算复杂度，使其能够处理大规模代码。欠近似方法则保证了检测结果的可靠性，避免了误报。

关键设计：Pulse Infinite的具体技术细节包括：1) 使用分离逻辑（Separation Logic）来形式化程序的语义。2) 使用归纳推理（Inductive Reasoning）来证明程序的非终止性。3) 设计了一种新的抽象域（Abstract Domain）来表示程序的状态。4) 采用了一种基于策略（Policy-based）的搜索算法来加速证明过程。

📊 实验亮点

Pulse Infinite成功应用于超过一亿行代码的开源和专有软件，包括C、C++和Hack等多种编程语言。实验结果表明，该工具能够有效地检测出真实代码库中的非终止问题，并发现了30多个以前未知的bug。这证明了Pulse Infinite在处理大规模代码时的有效性和实用性，为非终止性检测领域树立了新的标杆。

🎯 应用场景

该研究成果可应用于软件质量保证、安全漏洞检测等领域。通过自动检测大型代码库中的非终止问题，可以帮助开发者及时发现和修复潜在的缺陷，提高软件的可靠性和安全性。此外，该技术还可以用于编译器优化，避免因无限循环或递归导致的程序崩溃。

📄 摘要（原文）

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.