LoAT (**Lo**op **A**cceleration **T**ool, formerly known as **Lo**wer Bounds **A**nalysis **T**ool) is a fully automated tool to analyze programs operating on integers.
Currently, it supports the inference of **lower bounds** on the worst-case runtime complexity and **non-termination proving**.

LoAT uses a calculus for modular loop acceleration and a variation of ranking functions to deduce lower bounds and to prove non-termination.

The tool is based on the recurrence solver PURRS and the SMT solvers Yices and Z3.

# Downloading LoAT

Here you can find the latests releases of LoAT.

# Input Formats

To analyze programs with LoAT, they need to be represented as *Integer Transition Systems*.
It supports the most common formats for such systems.

## SMTLIB

LoAT can parse the SMTLIB-format used in the category *Termination of Integer Transition Systems* at the annual *Termination and Complexity Competition*.

## KoAT

LoAT also supports an extended version of KoAT’s input format, which is also used in the category *Complexity of Integer Transition Systems* at the annual *Termination and Complexity Competition*.

In this extension, rules can be annotated with polynomial costs:

```
l1(A,B) -{A^2,A^2+B}> Com_2(l2(A,B),l3(A,B)) :|: B >= 0
```

Here, `A^2`

and `A^2+B`

are lower and upper bounds on the cost of the rule.
The upper bound is ignored by LoAT.
The lower bound has to be non-negative for every model of the transition’s guard.

## T2

LoAT also comes with experimental support for the native input format of T2.

# Publications

The techniques implemented in LoAT are described in the following publications (in chronological order):

- Lower Runtime Bounds for Integer Programs

F. Frohn, M. Naaf, J. Hensel, M. Brockschmidt, and J. Giesl

IJCAR ‘16 - Proving Non-Termination via Loop Acceleration

F. Frohn and J. Giesl

FMCAD ‘19 - Inferring Lower Runtime Bounds for Integer Programs

F. Frohn, M. Naaf, M. Brockschmidt, and J. Giesl

ACM Transactions on Programming Languages and Systems, 42(3), 2020 - A Calculus for Modular Loop Acceleration

F. Frohn

TACAS ‘20

Winner of the EASST Best Paper Award

# Awards

In 2020, LoAT competed as standalone tool at the *Termination and Complexity Competition* for the first time.

- best tool for proving non-termination in the category
*Termination of Integer Transition Systems*at the*Termination and Complexity Competition 2020* - 2nd place in the category
*Termination of Integer Transition Systems*at the*Termination and Complexity Competition 2020* - best tool for proving non-termination in the category
*Termination of Integer Transition Systems*at the*Termination and Complexity Competition 2021* - 2nd place in the category
*Termination of Integer Transition Systems*at the*Termination and Complexity Competition 2021*

Since 2016, AProVE is using LoAT as backend to prove lower bounds on the runtime complexity of integer transition systems. In this constellation, AProVE and LoAT won the following awards:

- 1st place in the category
*Complexity of Integer Transition Systems*at the*Termination and Complexity Competition 2016* - 1st place in the category
*Complexity of Integer Transition Systems*at the*Termination and Complexity Competition 2017* - 1st place in the category
*Complexity of Integer Transition Systems*at the*Termination and Complexity Competition 2018* - 1st place in the category
*Complexity of Integer Transition Systems*at the*Termination and Complexity Competition 2019*

Since 2021, AProVE is using LoAT in its backend to prove non-termination of C programs (besides T2). In this constellation AProVE, LoAT, and T2 won the following awards:

- 2nd place in the Category Termination at the
*Competition on Software Verification 2022*

# Build

Install docker and run `./compile_static_binary`

. Then the path to the binary is `./build/static/release/loat-static`

.

If you experience any problems, contact florian.frohn [at] cs.rwth-aachen.de.