Non-Termination Proving: 100 Million LoC and Beyond
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912573420470272 |
|---|---|
| author | Vanegue, Julien Villard, Jules O'Hearn, Peter Raad, Azalea |
| author_facet | Vanegue, Julien Villard, Jules O'Hearn, Peter Raad, Azalea |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_05293 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Non-Termination Proving: 100 Million LoC and Beyond Vanegue, Julien Villard, Jules O'Hearn, Peter Raad, Azalea Programming Languages Computation and Language Software Engineering D.3; F.3 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. |
| title | Non-Termination Proving: 100 Million LoC and Beyond |
| topic | Programming Languages Computation and Language Software Engineering D.3; F.3 |
| url | https://arxiv.org/abs/2509.05293 |