Termination Analysis by Learning Terminating Programs

TL;DR

This paper introduces a novel termination analysis method that learns from finite sample traces represented as lassos, constructing terminating programs and verifying their representativeness to assess overall program termination.

Contribution

It proposes a new two-step approach combining learning from sample traces with formal verification, enhancing existing termination analysis techniques.

Findings

The approach can learn terminating programs from sample traces.

Experimental results show potential usefulness in termination analysis.

The method complements existing approaches with a learning-based perspective.

Abstract

We present a novel approach to termination analysis. In a first step, the analysis uses a program as a black-box which exhibits only a finite set of sample traces. Each sample trace is infinite but can be represented by a finite lasso. The analysis can "learn" a program from a termination proof for the lasso, a program that is terminating by construction. In a second step, the analysis checks that the set of sample traces is representative in a sense that we can make formal. An experimental evaluation indicates that the approach is a potentially useful addition to the portfolio of existing approaches to termination analysis.