Neural Termination Analysis

We introduce a novel approach to the automated termination analysis of computer programs: we train neural networks to behave as ranking functions. Ranking functions map program states to values that are bounded from below and decrease as the program runs. The existence of a valid ranking function proves that the program terminates. While existing methods usually construct ranking functions from source or machine code using symbolic reasoning, we propose a lightweight method that learns them from executions traces. We train a neural network so that its output decreases along sampled executions as a ranking function would; then, we use symbolic reasoning to verify whether it generalises to all possible executions. We demonstrate that, thanks to the ability of neural networks to generalise well, our method succeeds over a wide variety of programs. This includes programs that use data structures. We have built a prototype analyser for Java bytecode and show the efficacy of our method over a standard dataset of benchmarks.