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