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.

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.