Modular Termination Analysis

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.


Paper

Synthesising Interprocedural Bit-Precise Termination Proofs
H. Chen, C. David, D. Kroening, P. Schrammel, and B. Wachter
ASE'15
Extended version on arXiv


Tool

Our tool is maintained in a git repository. To get the tool, follow these instructions:

Installation:
git clone https://github.com/diffblue/2ls
cd 2ls
./install.sh


Basic usage:
./2ls file.c --termination

See the 2LS website for further information.


Experiments

There is a package for reproducing the experiments reported in the paper.

Moreover, we provide the results tables, and notes on issues encountered with the tools that we tried.