Skip to the content.

LoAT (Loop Acceleration Tool, formerly known as Lower Bounds Analysis Tool) 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.


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


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.


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


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


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

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:

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:


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]