This page contains additional information on our article “Modular Automatic Complexity Analysis of Recursive Integer Programs”. The full version of our article is also available on ArXiv. More precisely, we describe our implementation and our experiments.
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 KoAT2 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 as described here.
Experiments
To evaluate the power and performance of our approach we provided 45 new benchmarks of ITSs with non-tail recursion, including the leading example of our paper. Detailed information about the new examples can be found here.
Furthermore, we tested KoAT on the ITS benchmark set from the TPDB. We refer to this set as Complexity_ITS (CITS), and it consists of 816 integer programs.
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). In the following, we refer to our novel implementation as “KoAT2” to distinguish it clearly from KoAT1.
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.
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.
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.
A timeout of 5 minutes was enforced for every tool and program.
For KoAT2 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.
Evaluation: ITS with Function Calls
The following table depicts the results of KoAT compared to the tools CoFloCo and KoAT1 on the 45 new function call benchmarks and on the benchmark set Complexity_ITS..
Please click on the tool names to obtain a detailed list of all results. The number in brackets only considers the 45 new ρ-ITS benchmarks.
| Tool | O(1) | O(log(n)) | O(n) | O(n²) | O(nᵏ), k>2 | < ∞ | AVG⁺(s) | AVG(s) |
|---|---|---|---|---|---|---|---|---|
| KoAT | 128 | 11 | 281 (18) | 121 (8) | 28 (4) | 583 (34) | 3.45 | 21.78 |
| KoAT1 | 132 | 0 | 231 (15) | 108 (4) | 16 (2) | 499 (24) | 0.64 | 8.06 |
| CoFloCo | 125 | 0 | 234 (1) | 95 | 10 (1) | 464 (2) | 3.19 | 16.38 |
Limitations of KoAT
Of course, there are several limitations of our approach and its implementation. Currently, KoAT can only successfully analyze programs where the arguments in recursive calls decrease w.r.t. a linear polynomial ranking function (see, e.g., fc21.koat). Moreover, our approach via ρ-RFs can only infer polynomial or exponential bounds. So for example, we cannot obtain precise bounds for recursive algorithms with sublinear (e.g., logarithmic or square-root, as in fc04.koat or fc22.koat) or factorial runtime (see, e.g., fc12.koat). Our implementation only computes logarithmic bounds for subprograms that are twn-loops. Another restriction is that we can only lift local size bounds of a certain form to global size bounds (see, e.g., fc15.koat).
In addition, KoAT may fail to infer finite runtime bounds for several other reasons, e.g., there are examples which would have to be augmented with stronger invariants in order to make our approach succeed (see, fc24.koat and fc25.koat). Moreover, KoAT uses over-approximations at several places which increases the performance but leads to less precise upper bounds (e.g., KoAT uses global runtime bounds instead of local runtime bounds in the computation of size bounds, see fc20.koat). While KoAT does not specialize in amortized complexity analysis, it employs a form of normalization which may sometimes derive amortized complexity bounds (see, e.g., fc23.koat).