# Proving Non-Termination and Lower Runtime Bounds with LoAT (System Description)

arXiv: https://arxiv.org/abs/2202.04546 · HTML: https://mlsanity.com/paper/2202.04546/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Feb 2022.

## Built on by (most cited first, 1 of 1)

- [A Machine Learning-based Approach for Solving Recurrence Relations and its use in Cost Analysis of Logic Programs](https://mlsanity.com/paper/2405.06972/) (2024)

## Abstract (arXiv)

We present the new version of the Loop Acceleration Tool (LoAT), a powerful tool for proving non-termination and worst-case lower bounds for programs operating on integers. It is based on a novel calculus for loop acceleration, i.e., transforming loops into non-deterministic straight-line code, and for finding non-terminating configurations. To implement it efficiently, LoAT uses a new approach based on SMT solving and unsat cores. An extensive evaluation shows that LoAT is highly competitive with other state-of-the-art tools for proving non-termination. While no other tool is able to deduce worst-case lower bounds for full integer programs, we also demonstrate that LoAT significantly outperforms its predecessors.