# Proving Non-Termination via Loop Acceleration

## TL;DR

This paper introduces a novel approach to proving non-termination of integer programs using loop acceleration, which also helps find paths to other non-terminating loops, enhancing automated analysis.

## Contribution

It presents the first non-termination proof method based on loop acceleration, including a new invariant inference technique and a unified transformation framework.

## Key findings

- The approach is fully automated and competitive with existing methods.
- The technique successfully proves non-termination in various benchmark programs.
- It can also accelerate loops to discover non-termination paths.

## Abstract

We present the first approach to prove non-termination of integer programs that is based on loop acceleration. If our technique cannot show non-termination of a loop, it tries to accelerate it instead in order to find paths to other non-terminating loops automatically. The prerequisites for our novel loop acceleration technique generalize a simple yet effective non-termination criterion. Thus, we can use the same program transformations to facilitate both non-termination proving and loop acceleration. In particular, we present a novel invariant inference technique that is tailored to our approach. An extensive evaluation of our fully automated tool LoAT shows that it is competitive with the state of the art.