Neural Termination Analysis
This work provides a new method for formally verifying program termination, which is a critical problem for software engineers and developers, especially for programs with complex control flow and nonlinear expressions.
This paper introduces a new method for automated program termination analysis by using neural networks to represent ranking functions. The neural network is trained on sampled execution traces to ensure its output decreases, and then formally verified using symbolic reasoning to generalize to all executions, resulting in a formal termination certificate. This approach successfully analyzes programs with disjunctions in loop conditions and nonlinear expressions, which are challenging for existing state-of-the-art tools.
We introduce a novel approach to the automated termination analysis of computer programs: we use neural networks to represent ranking functions. Ranking functions map program states to values that are bounded from below and decrease as a program runs; the existence of a ranking function proves that the program terminates. We train a neural network from sampled execution traces of a program so that the network's output decreases along the traces; then, we use symbolic reasoning to formally verify that it generalises to all possible executions. Upon the affirmative answer we obtain a formal certificate of termination for the program, which we call a neural ranking function. We demonstrate that thanks to the ability of neural networks to represent nonlinear functions our method succeeds over programs that are beyond the reach of state-of-the-art tools. This includes programs that use disjunctions in their loop conditions and programs that include nonlinear expressions.