@article{10.1145/3689720,
author = {Raad, Azalea and Vanegue, Julien and O’Hearn, Peter},
title = {Non-termination Proving at Scale},
year = {2024},
issue_date = {October 2024},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
volume = {8},
number = {OOPSLA2},
url = {https://doi.org/10.1145/3689720},
doi = {10.1145/3689720},
abstract = {Program termination is a classic non-safety property whose falsification cannot in general be witnessed by a finite trace. This makes testing for non-termination challenging, and also a natural target for symbolic proof. Several works in the literature apply non-termination proving to small, self-contained benchmarks, but     it has not been developed for large, real-world projects; as such, despite its allure, non-termination proving has had limited practical impact.     We develop a compositional theory for non-termination proving, paving the way for its scalable application to large codebases.     Discovering non-termination is an under-approximate problem, and we present UNTer, a sound and complete under-approximate logic for proving non-termination. We then extend UNTer with separation logic and develop UNTerSL for heap-manipulating programs, yielding a compositional proof method amenable to automation via under-approximation and bi-abduction.     We extend the Pulse analyser from Meta and develop Pulse∞, an automated, compositional prover for non-termination based on UNTerSL. We have run Pulse∞ on large codebases and libraries, each comprising hundreds of thousands of lines of code, including OpenSSL, libxml2, libxpm and CryptoPP; it discovered several previously-unknown non-termination bugs and have reported them to developers of these libraries.},
journal = {Proc. ACM Program. Lang.},
month = oct,
articleno = {280},
numpages = {29},
keywords = {Divergence, incorrectness logic, non-termination, under-approximation}
}