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

TL;DR

This paper introduces LoAT, a new tool that proves non-termination and lower runtime bounds for integer programs using a novel loop acceleration calculus and SMT solving, outperforming existing tools.

Contribution

The paper presents a novel calculus for loop acceleration and an efficient implementation of LoAT that advances the state-of-the-art in proving non-termination and lower bounds.

Findings

LoAT effectively proves non-termination for various programs.

LoAT outperforms existing tools in proving non-termination.

LoAT uniquely deduces worst-case lower bounds for full integer programs.

Abstract

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.