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