用形式化证明检测上亿行代码中的无限循环，发现30多个未知漏洞。
Non-Termination Proving: 100 Million LoC and Beyond
- 通过组合式与近似下界分析，实现大规模代码的非终止性证明。
- 在超1亿行C/C++/Hack代码中识别出30多个未被发现的无限循环问题。
- 适合大型软件公司做静态分析，提升系统可靠性。
我们报告了名为Pulse Infinite的工具，该工具利用证明技术来识别大型程序中的非终止（发散）行为。Pulse Infinite采用组合式与近似下界方法：前者支持可扩展性，后者确保发散性证明的正确性。以往研究集中在数百行代码的小型基准测试，规模限制了其实际应用价值——单个公司代码量可达数千万甚至上亿行。我们对超过一亿行开源及私有代码（使用C、C++和Hack语言编写）应用Pulse Infinite，发现了30多个此前未知的发散问题，确立了真实世界代码库中检测非终止性的新基准。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。