Chen, Hong-Yi, David, Cristina, Kroening, Daniel, Schrammel, Peter and Wachter, Björn (2015) Synthesising interprocedural bit-precise termination proofs. In: Automated Software Engineering (ASE), 2015 30th IEEE/ACM International Conference on. IEEE, pp. 53-64. ISBN 9781509000258

PDF - Accepted Version Restricted to SRO admin only Download (401kB)

Abstract

Proving program termination is key to guaranteeing absence of undesirable behaviour, such as hanging programs and even security vulnerabilities such as denial-of-service attacks. To make termination checks scale to large systems, interprocedural termination analysis seems essential, which is a largely unexplored area of research in termination analysis, where most effort has focussed on 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 that our tool 2LS outperforms state-of-the-art alternatives, and demonstrate the clear advantage of interprocedural reasoning over monolithic analysis in terms of efficiency, while retaining comparable precision.

Item Type:	Book Section
Keywords:	termination analysis, interprocedural analysis, template-based synthesis, lexicographic ranking functions, precondition inference
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:	09 May 2016 06:58
Last Modified:	09 May 2016 06:58
URI:	http://srodev.sussex.ac.uk/id/eprint/59920

View download statistics for this item

📧 Request an update