Proving Non-Termination and Lower Runtime Bounds with LoAT

This is the empirical evaluation of the paper Proving Non-Termination and Lower Runtime Bounds with LoAT. You can find the source code for our tool LoAT at GitHub.

Moreover, we refer to the general LoAT website for further information.

Running LoAT

We provide a pre-compiled binary of LoAT (Linux, 64 bit).

Invocation for proving non-termination: ./loat-static --timeout $TO --mode non_termination $INPUT
Invocation for proving worst-case lower bounds on the runtime complexity: ./loat-static --timeout $TO $INPUT
LoAT can parse three different input formats:

.koat
the format from the category Complexity of Integer Transition Systems of the anual Termination and Complexity Competition
.smt2
the format from the category Termination of Integer Transition Systems of the anual Termination and Complexity Competition
.t2 (experimental)
the native format of the tool T2

Evaluation

StarExec Bundles

We provide StarExec bundles for all tools used in our evaluation.

LoAT '22, configuration loat_nonterm_proofout or loat_cpx_proofout, respectively
LoAT '19, configuration proofout
LoAT '20, configuration proofout
iRankFinder, configuration competition
KoAT, configuration cfr_mprf_five
T2, configuration default fixed
VeryMax, configuration termcomp2019_ITS

Results

Below we provide tables with the detailed results of our benchmarks:

Evaluation on the examples from the category Termination of Integer Transition Systems of the Termination Problems Data Base

Evaluation on the examples from the category Complexity of Integer Transition Systems of the Termination Problems Data Base