2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE) (2015)
Lincoln, NE, USA
Nov. 9, 2015 to Nov. 13, 2015
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/ASE.2015.10
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.
Context, Algorithm design and analysis, Encoding, Semantics, Computer crime, Computer bugs
H. Chen, C. David, D. Kroening, P. Schrammel and B. Wachter, "Synthesising Interprocedural Bit-Precise Termination Proofs (T)," 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), Lincoln, NE, USA, 2015, pp. 53-64.