Neural Termination Analysis

TL;DR

This paper presents a neural network-based method for automated program termination analysis, leveraging neural ranking functions trained on execution traces and verified symbolically, enabling analysis of complex programs with nonlinear and disjunctive conditions.

Contribution

The paper introduces neural ranking functions for termination analysis, combining neural network training with symbolic verification to handle nonlinear and disjunctive program features.

Findings

Successfully analyzes programs with nonlinear expressions.

Handles disjunctive loop conditions.

Outperforms existing tools on complex programs.

Abstract

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.