This page contains additional information on our article “Modular Automatic Complexity Analysis of Recursive Integer Programs”. More precisely, we describe our implementation and our experiments.
Implementation
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 15 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.
The table below presents the actual runtimes of the benchmarks along with the results produced by our tool KoAT. Here, n is the largest initial absolute value of all program variables.
| Benchmark | Runtime Complexity | KoAT |
|---|---|---|
| 1 | O(n) | O(n) |
| 2 | O(n) | O(n) |
| 3 | O(n) | O(n) |
| 4 | O(log(n)) | O(n) |
| 5 | O(EXP) | O(EXP) |
| 6 | O(n) | O(n) |
| 7 | O(n^2) | O(n^2) |
| 8 | O(EXP) | O(EXP) |
| 9 | O(EXP) | O(EXP) |
| 10 | O(n) | O(n) |
| 11 | O(n) | O(n) |
| 12 | O(log(n!)) | O(n*log(n)) |
| 13 | O(n^2) | O(n^2) |
| 14 | O(n^2) | O(n^2*log(n)) |
| 15 | O(log(n)) | ∞ |