About

KoAT (German: Komplexitäts-Analyse-Tool) is a tool to automatically infer complexity bounds for (probabilistic) integer programs, based on an alternating modular inference of upper runtime and size bounds for program parts.

Recently, we extended and reimplemented this approach in a new version of our open-source tool KoAT (sometimes called KoAT2). By inferring runtime bounds for individual subprograms one after the other, in the end we obtain a bound on the runtime complexity of the whole program. Currently, we have integrated two approaches to infer runtime bounds for subprograms:

Moreover, we integrated control-flow refinement via partial evaluation to improve the automatic complexity analysis of programs further (see here). Furthermore, we developed a novel procedure to infer size bounds by using closed forms (see here) which in particular is capable of handling programs with non-linear arithmetic.

Additionally, we introduced the notion of expected size which allowed us to extend our approach to the computation of upper bounds on the expected runtimes of probabilistic programs (see here).

You can easily test KoAT via our web interface. However, there exist multiple ways to work with KoAT (see getting started).

KoAT is developed and maintained by LuFG i2 Aachen. It is used as a backend for the automated termination tool AProVE. If you encounter any difficulties, either use GitHub issues or contact us via aprove [at] i2.informatik.rwth-aachen.de.