Termination Proofs from Tests

We show how a test suite for a sequential program can be profitably used to construct a termination proof. In particular,we describe an algorithm TpT for constructing a termination proof of a program based on information derived from testing it. TpT iteratively calls two phases: (a) an infer phase, and (b) a validate phase. In the infer phase, machine learning, in particular, linear regression is used to efficiently compute a candidate loop bound for every loop in the program. These loop bounds are verified for correctness by an of-the-shelf checker. If a loop bound is invalid, then the safety checker provides a test or a counterexample that is used to generate more data which is subsequently used by the next infer phase in order to compute better estimates for loop bounds. On the other hand, if all loop bounds are valid, then we have a proof of termination. This separation of the infer phase from the validate phase allows our approach to handle more expressive syntax than previous approaches for termination of numerical programs. We also describe a simple extension to our approach that allows us to infer polynomial loop bounds automatically. We have evaluated TpT on two benchmark sets, micro benchmarks obtained from recent literature on program termination, and Windows device drivers. Our results are promising on the micro benchmarks, we show that TpT is able to prove termination on 15% more benchmarks than any previously known technique, and our evaluation on Windows device drivers demonstrates TpT’s ability to analyse and scale to industrial strength applications.