Lifted termination analysis by abstract interpretation and its applications

Abstract

This paper is focused on proving termination for program families with numerical features by using abstract interpretation. Furthermore, we present an interesting application of the above lifted termination analysis for resolving “sketches”, i.e. partial programs with missing numerical parameters (holes), such that the resulting complete programs always terminate. To successfully address the above problems, we employ an abstract interpretation-based framework for inferring sufficient preconditions for termination of single programs that synthesizes piecewise-defined ranking functions.

We introduce a novel lifted decision tree domain for termination, in which decision nodes contain linear constraints defined over numerical features and leaf nodes contain piecewise ranking functions defined over program variables. Moreover, we encode a program sketch as a program family, thereby allowing the use of the lifted termination analysis as a program sketcher. In particular, we aim to find the variants (family members) that terminate under all possible inputs, which represent the correct sketch realizations.

We have implemented an experimental lifted termination analyzer, called SPLFuncTion, for proving termination of #if-based C program families and for termination-directed resolving of C program sketches. We have evaluated our approach by a set of loop benchmarks from SV-COMP, and experimental results confirm the effectiveness our approach.