Abstract

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 ranking function proves that the program terminates.  We learn ranking functions from execution traces by training a neural network so that its output decreases along the sampled executions; then, we use symbolic reasoning to formally verify that it generalises to all possible executions.  We demonstrate that, thanks to the ability of neural networks to represent highly complex functions, our method succeeds over programs that are beyond the reach of state-of-the-art tools.  This includes programs that use loop guards with disjunctions and programs that exhibit nonlinear behaviour.