Non-Termination Proving: 100 Million LoC and Beyond

Understand

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.