Chen, Hong-Yi, David, Cristina, Kroening, Daniel, Schrammel, Peter and Wachter, Björn (2017) Bit-precise procedure-modular termination analysis. ACM Transactions on Programming Languages and Systems, 40 (1). pp. 1-38. ISSN 0164-0925
![]() |
PDF (© ACM, 2017. This is the author's version of the work. It is posted here by permission of ACM. Not for redistribution. The definitive version was published in ACM Transactions on Programming Languages and Systems at https://doi.org/10.1145/3121136)
- Accepted Version
Download (526kB) |
Abstract
Non-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.
Item Type: | Article |
---|---|
Keywords: | termination analysis, interprocedural analysis, bit-precise analysis, synthesis |
Schools and Departments: | School of Engineering and Informatics > Informatics |
Subjects: | Q Science > QA Mathematics > QA0075 Electronic computers. Computer science |
Depositing User: | Peter Schrammel |
Date Deposited: | 02 Aug 2017 08:22 |
Last Modified: | 27 Mar 2018 16:16 |
URI: | http://srodev.sussex.ac.uk/id/eprint/69530 |
View download statistics for this item
📧 Request an update