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 and disprove satisfiability.

LoAT is based on a variety of techniques:

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

Downloading LoAT

Here you can find the latest releases of LoAT, including nightly releases. Older releases can be found here.

Using LoAT

A typical usage of LoAT for analyzing safety/satisfiability looks as follows:

$ loat-static --engine abmc --mode safety example.smt2
unsat

LoAT:  595a95cf76ac783e87ce760ec4ccfeca66d93d43
Yices: 2.6.5
       build mode: release
       build arch: x86_64-pc-linux-gnu
       build date: 2024-08-15
SwInE: 141d02206bd74f86a01fa57c2dc9ed193abbfe6e

Here, unsatisfiability of the runnning example from our paper on ABMC has been proven.

A typical usage of LoAT for analyzing termination looks as follows:

loat-static --format ari --engine adcl --mode termination example.ari
NO

LoAT:  595a95cf76ac783e87ce760ec4ccfeca66d93d43
Yices: 2.6.5
       build mode: release
       build arch: x86_64-pc-linux-gnu
       build date: 2024-08-15
SwInE: 141d02206bd74f86a01fa57c2dc9ed193abbfe6e

Here, non-termination of the benchmark non_term.t2.ari from the Termination Problems Database, the benchmark collection of the annual Termination and Complexity Competition (TermComp) has been proven.

See loat-static --help for more information.

Input Format for Transition Systems

LoAT can parse the ARI-format used at TermComp.

For examples, we refer to the TPDB benchmarks for termination and for complexity analysis.

Input Format for Constrained Horn Clauses

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

For examples, we refer to the CHC-COMP benchmarks from 2024.

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.

Moreover, earlier versions of LoAT could parse the SMTLIB-format for programs with procedures, the KoAT format, and the C-Integer format that had been used at TermComp. Since all of these formats have been discontinued at TermComp, they are no longer supported.

Publications

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

Citing LoAT

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

Awards

LoAT competes in several competitions.

CHC-COMP

LoAT competes in the category LIA-Lin (linear clauses with linear integer arithmetic) of the CHC Competition since 2023.

TermComp

LoAT competes in several categories of the Termination and Complexity Competition since 2016.

From 2016 until 2019, AProVE was using LoAT as backend to prove lower bounds on the runtime complexity of integer transition systems. Nowadays, LoAT and KoAT compete together in this category.

Since 2022, AProVE is using LoAT in its backend to prove non-termination of C programs.

SV-COMP

Together with AProVE, LoAT competes in the category Termination of the Competition on Software Verification

Build

Think about using one of our releases instead. If that’s not an option, proceed as follows:

  1. install Docker
  2. download the latest docker container with pre-installed dependencies via docker pull loat/loat-base:$VERSION
  3. log in to the docker container via docker run -it loat/loat-base:$VERSION bash
  4. git clone https://github.com/LoAT-developers/LoAT.git
  5. mkdir LoAT/build
  6. cd LoAT/build
  7. cmake -DCMAKE_BUILD_TYPE=$TYPE .. where $TYPE is either Release or Debug, depending on your use case
  8. make -j$(nproc)
  9. if everything worked, ./loat-static --help should print a help message