Non-Termination Proving at Scale

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. A number of 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 a consequence, 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 completeunder-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 (LOC), including OpenSSL, libxml2, CryptoPP and libxpm; we discovered several previously-unknown non-termination bugs and have reported them to developers of these libraries.

Paper

Artifact

People