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:
- Multiphase Linear Ranking Functions (MΦRFs see here)
- Triangular Weakly Non-Linear Loops (twn-loops see here)
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).