Skip to content
Branch: master
Go to file
Code

README.md

LoAT -- the Loop Acceleration Tool

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 (in the branch nonterm).

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.

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

The branch nonterm 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):

Awards

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:

Build

Unfortunately, building LoAT is rather complex, so please consider using our pre-compiled releases. If you need a different version, write an email to ffrohn [at] mpi-inf.mpg.de.

To compile LoAT, you will need the following libraries (and their dependencies, including CLN, NTL, and giac):

To install Z3, download and unpack the latest Z3 release and add /path/to/z3/bin to your PATH. After installing all dependencies, run:

mkdir build && cd build && cmake .. && make

If you experience any problems, contact ffrohn [at] mpi-inf.mpg.de.

You can’t perform that action at this time.