Synthesising interprocedural bit-precise termination proofs

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

[img] PDF - Accepted Version
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: 01 May 2019 11:24
URI: http://sro.sussex.ac.uk/id/eprint/59920

View download statistics for this item

📧 Request an update