Synthesising interprocedural bit-precise termination proofs

Conference item

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.

Authors: Chen, H; David, C; Kroening, D; Schrammel, P; Wachter, B

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: IEEE
• Host title: 30th IEEE/ACM International Conference on Automated Software Engineering (ASE)
• Journal: 30th IEEE/AC30th IEEE/ACM International Conference on Automated Software Engineering (ASE)
• Pages: 53-64
• Publication date: 2016-01-04
• DOI: 10.1109/ASE.2015.10
• ISBN: 9781509000241
• Keywords: SBTMR