Synthesising Interprocedural Bit-Precise Termination Proofs (extended version)

TL;DR

This paper introduces a modular interprocedural termination analysis for C programs that synthesizes bit-precise termination proofs, improving efficiency and maintaining precision compared to existing methods.

Contribution

It presents a novel template-based interprocedural summarisation approach combining forward analysis with precondition inference for termination, specifically for large C programs.

Findings

Our tool 2LS outperforms state-of-the-art alternatives.

Interprocedural reasoning is more efficient than monolithic analysis.

The approach maintains high precision in termination proofs.

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.