Non-Termination Proving: 100 Million LoC and Beyond
This addresses the scalability limitations of prior non-termination proving tools, which were limited to small benchmarks, making it practical for real-world codebases with tens to hundreds of millions of lines of code.
The authors tackled the problem of proving non-termination (divergence) in large-scale software, developing Pulse Infinite to analyze over 100 million lines of code and identify over 30 previously unknown issues.
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.