paper.pdf (514.18 kB)
Bit-precise procedure-modular termination analysis
journal contribution
posted on 2023-06-09, 07:30 authored by Hong-Yi Chen, Cristina David, Daniel Kroening, Peter Schrammel, Björn WachterNon-termination is the root cause of a variety of program bugs, such as hanging programs and denial-of-service vulnerabilities. This makes an automated analysis that can prove the absence of such bugs highly desirable. To scale termination checks to large systems, an interprocedural termination analysis seems essential. This is a largely unexplored area of research in termination analysis, where most effort has focussed on small but difficult single-procedure problems. We present a modular termination analysis for C programs using template-based interprocedural summarisation. Our analysis combines a context-sensitive, over-approximating forward analysis with the inference of under-approximating preconditions for termination. Bit-precise termination arguments are synthesised over lexicographic linear ranking function templates. Our experimental results show the advantage of interprocedural reasoning over monolithic analysis in terms of efficiency, while retaining comparable precision.
History
Publication status
- Published
File Version
- Accepted version
Journal
ACM Transactions on Programming Languages and SystemsISSN
0164-0925Publisher
ACM PressExternal DOI
Issue
1Volume
40Page range
1-38Department affiliated with
- Informatics Publications
Full text available
- Yes
Peer reviewed?
- Yes
Legacy Posted Date
2017-08-02First Open Access (FOA) Date
2017-12-12First Compliant Deposit (FCD) Date
2017-08-01Usage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC