Synthesising Interprocedural Bit-Precise Termination Proofs
Peter Schrammel, Oxford
Date and Time
Wednesday, November 4th, 2015 at 14:15.
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.
This talk presents a modular termination analysis for C programs. The analysis generates a sequence of logical formulas with existentially quantified predicates that are solved by a synthesis-based program analysis engine. By these means, a context-sensitive, over-approximating forward analysis with the inference of under-approximating preconditions for termination is performed, where bit-precise termination arguments are synthesised over lexicographic linear ranking function templates. The experimental results with our tool 2LS demonstrate the clear advantage of interprocedural reasoning over monolithic analysis in terms of efficiency, while retaining comparable precision.