LoAT

LoAT (Loop Acceleration Tool) is a fully automated tool to analyze transition systems and linear Constrained Horn Clauses (CHCs) with integer variables. For transition systems, it supports the inference of lower bounds on the worst-case runtime complexity and non-termination proving. For CHCs, it can prove unsatisfiability.

LoAT is based on a calculus for modular loop acceleration. Loop acceleration transforms certain simple relations into first-order formulas that describe their transitive closure. To lift loop acceleration to more complex formalisms (like transition systems or CHCs), earlier versions of LoAT used the framework described in this paper. Current versions use a novel calculus called ADCL instead.

LoAT uses the recurrence solver PURRS, the SMT solvers Yices and Z3, and the automata-library libFAUDES.

Downloading LoAT

Here you can find the latests releases of LoAT. Older releases can be found here.

Using LoAT

To choose the goal of your analysis, please use one of the following command-line option

Currently, reachability / unsatisfiability is supported for CHCs only, as LoAT’s input formats for transition systems do not allow for specifying error states.

Input Formats for Transition Systems

LoAT supports the most common formats for Integer Transition Systems.

SMTLIB

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

To use this format, please use the command-line option --format its.

C Integer Programs

LoAT can parse the C Integer Programs used in the category Termination of C Integer Programs at the annual Termination and Complexity Competition.

To use this format, please use the command-line option --format c.

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}> l2(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.

To use this format, please use the command-line option --format koat.

Input Format for Constrained Horn Clauses

LoAT can parse the SMTLIB-format used at the annual CHC-COMP.

To use this format, please use the command-line option --format horn.

Discontinued Features

Earlier versions of LoAT could analyze the complexity of non-tail-recursive transition systems, i.e., systems with transitions like f(x) -> Com2(f(x-1), f(x-2)) :|: x>1. Such systems are no longer supported. If you are interested in analyzing such systems, please use the release that was published with our TOPLAS ‘20 paper. A link to this release, as well as further information about using it, can be found here.

Publications

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

Citing LoAT

If you refer to LoAT in your paper, please cite our IJCAR ‘22 system description

Awards

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

From 2016 until the last run of this category in 2019, AProVE was 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:

Build

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