KoAT: Automatic Complexity and Termination Analysis of Integer Programs

This page contains additional information on our article “KoAT: Automatic Complexity and Termination Analysis of Integer Programs”. More precisely, we describe our implementation and our experiments. A permanent artifact to reproduce our results can be found here.

Implementation

The source code of our new version of KoAT corresponding to our paper can be found here. The most recent official version of KoAT is available on GitHub. See our documentation for a list of external tools and libraries used by KoAT.

Our implementation can be executed via the web interfaces, via a Docker image, and via the provided static binary. A Docker image containing KoAT and a static binary of the new release can be downloaded here. A web interface using this new release is provided here.

Concerning the input format, for integer programs we extended the corresponding input format from the Termination and Complexity Competition by (possibly recursive) function calls as described here. Note that a disjunction is modeled by two parallel transitions with the same update, and negations are modeled by flipping every comparator (i.e., ¬(x<y) is equivalent to x≥y). Additionally, we also allow for costs in transitions.

Experiments

To evaluate the power and performance of our approach we compared KoAT against the participating tools in the categories Complexity and Termination of the TermComp. Here, the set of benchmarks Complexity_ITS consists of 838 integer programs whereas Termination_ITS consists of 1222 benchmarks.

We compare the results of our tool KoAT to that of other state-of-the-art tools for complexity analysis such as CoFloCo and KoAT1 (the original implementation of KoAT). Moreover, we compare to the tools which participated in the 2025 TermComp:

All tools were run inside an Ubuntu Docker container on a machine with an AMD Ryzen 7 3700X octa-core CPU and 8 GB of RAM. The benchmarks were evaluated in parallel in different containers, where each container is limited to 2 CPU cores. In particular, the runtimes of the tools include the times to start and remove the container. A timeout of 1 minute was enforced for every tool and program.

Complexity_ITS

Here, we provide the results of our experiments on Complexity_ITS. We compare the runtime bounds computed by the tools asymptotically as functions which depend on the largest initial absolute value n of all program variables. We give both the average runtime of each tool on all runs and the average runtime on successful runs, i.e., where the tool inferred a finite runtime bound before reaching the timeout. For KoAT we use the following configuration: multiphase ranking-functions of depth 5, control-flow refinement, twn and unsolvable loops (in particular, logarithmic runtime bounds for such loops), and size bounds for solvable commuting simple cycles.

Please click on the tool names to obtain a detailed list of all results.

Tool O(1) O(log(n)) O(n) O(n²) O(nᵏ), k>2 < ∞ AVG⁺(s) AVG(s)
KoAT 132 9 261 113 24 548 2.81 7.17
KoAT1 132 0 216 104 14 475 0.67 3.33
CoFloCo 125 0 230 93 9 457 1.50 5.38

Termination_ITS

Here, we provide the results of our experiments on Termination_ITS. We give both the average runtime of each tool on all runs and the average runtime on successful runs, i.e., where the tool inferred a finite runtime bound before reaching the timeout. For KoAT we use the following configuration: multiphase ranking-functions of depth 5, control-flow refinement, twn and unsolvable loops (in particular, logarithmic runtime bounds for such loops).

Please click on the tool names to obtain a detailed list of all results.

Result T2 iRankFinder VeryMax MuVal KoAT LoAT Golem
Terminating 606 632 627 515 635 2 0
Non-Terminating 422 385 364 448 0 522 350
Total 1028 1017 991 963 635 524 350
AVG⁺(s) 2.03 5.45 6.67 3.96 1.96 1.38 2.42
AVG(s) 7.08 12.99 14.51 15.51 7.94 11.24 9.87