Dear Spiral user, We’re pleased to introduce Helix, https://helix.imperial.ac.uk/ Imperial’s new repository for research datasets. Please use Helix for all future dataset deposits. There is no change to Spiral - continue depositing as usual. For queries, contact the Research Data Management team at rdm-enquiries@imperial.ac.uk. Kind regards, the Spiral Team. The Spiral team
Non-termination proving at scale
File(s)
3689720.pdf (1.01 MB)
Published version
Author(s)
Raad, Azalea
Vanegue, Julien
O’Hearn, Peter
Type
Journal Article
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 onx 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; we discovered several previously-unknown non-termination bugs and have reported them to developers of these libraries.
1 Introduction
Date Issued
2024-10-08
Date Acceptance
2024-08-18
Citation
Proceedings of the ACM on Programming Languages, 2024, 8 (OOPSLA2), pp.246-274
URI
URL
DOI
ISSN
2475-1421
Publisher
Association for Computing Machinery (ACM)
Start Page
246
End Page
274
Journal / Book Title
Proceedings of the ACM on Programming Languages
Volume
8
Issue
OOPSLA2
Copyright Statement
© 2024 Owner/Author. This work is licensed under a Creative Commons Attribution International 4.0 License.
License URL
Publication Status
Published
Article Number
280
Date Publish Online
2024-10-08