This web site contains additional information on our article “Improving Automatic Complexity Analysis of Integer Programs”. More precisely, we describe our implementation and our experiments.
Implementation
The source code of our official release version of KoAT2 can be found here. The most recent version of KoAT is also 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 both KoAT2 and iRankFinder and a static binary of the CFR-MΦRF5-release can be downloaded here. A web-interface using the CFR-MΦRF5-release is provided for integer programs and C programs.
Concerning the input format, for integer programs we use the corresponding input format from the Termination and Complexity Competition 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).
For C programs, we also use the corresponding input format from the Termination and Complexity Competition as described here. To analyze C programs, KoAT translates them into its format for integer programs using Clang and llvm2kittel.
Experiments
To evaluate the power and performance of our approach we tested it on two benchmark sets from the TPDB. The first set Complexity_ITS consists of 781 integer programs. The second set Complexity_C_Integer consists of 484 C programs on integers.
We compare the results of our tool KoAT2 in different configurations to that of other state-of-the-art tools such as KoAT1 (the original implementation of KoAT), CoFloCo, Loopus (only evaluated on Complexity_C_Integer), and MaxCore with CoFloCo as its backend (only evaluated on Complexity_C_Integer).
A timeout of 5 minutes was enforced for every tool and program.
Complexity_ITS
The programs of this benchmark set are integer programs in the format described in our paper. They can directly be analyzed by KoAT. For CoFloCo we used the corresponding configuration from the Termination and Complexity Competition 2019.
Please click on the tool names to obtain a detailed list of all results or to download the output of the corresponding configuration. Note that for all configurations of KoAT2, the integer programs in the output have been rendered as graphs using Graphviz.
| Tool | O(1) | O(n) | O(n²) | O(nᵏ), k>2 | O(EXP) | < ∞ | Avg. Runtime on runs with finite bound | Avg. Runtime |
|---|---|---|---|---|---|---|---|---|
| KoAT2 + MΦRF5 + CFR | 131 | 255 | 101 | 13 | 6 | 506 | 4.31 s | 26.50 s |
| KoAT2 + MΦRF5 + CFRSCC | 131 | 255 | 102 | 12 | 6 | 506 | 6.00 s | 27.47 s |
| KoAT2 + CFR | 131 | 245 | 101 | 10 | 6 | 493 | 5.00 s | 21.81 s |
| KoAT2 + CFRSCC | 131 | 245 | 101 | 9 | 6 | 492 | 6.37 s | 23.45 s |
| KoAT2 + MΦRF5 | 126 | 235 | 100 | 13 | 6 | 480 | 2.19 s | 13.32 s |
| KoAT1 | 132 | 214 | 104 | 14 | 5 | 469 | 0.65 s | 9.38 s |
| CFR + KoAT1 | 128 | 231 | 93 | 10 | 5 | 467 | 5.54 s | 40.81 s |
| CFR + KoAT2 | 130 | 231 | 93 | 6 | 6 | 466 | 10.44 s | 43.05 s |
| CoFloCo | 126 | 231 | 95 | 9 | 0 | 461 | 3.44 s | 18.40 s |
| KoAT2 | 126 | 218 | 97 | 10 | 6 | 457 | 2.29 s | 9.45 s |
Complexity_C_Integer
The programs of this benchmark set are C programs on integer values. For the analysis these are assumed to be mathematical integers. The tools MaxCore and Loopus can directly analyze these programs. For KoAT1 and KoAT2 they are translated into integer programs by using the tools Clang and llvm2kittel. For CoFloCo we again used the corresponding configuration that was used in the Termination and Complexity Competition 2019.
Please click on the tool names to obtain a detailed list of all results or to download the output of the corresponding configuration. Note that for all configurations of KoAT2, the integer programs in the output have been rendered as graphs using Graphviz.
| Tool | O(1) | O(n) | O(n²) | O(nᵏ), k>2 | O(EXP) | < ∞ | Avg. Runtime on runs with finite bound | Avg. Runtime |
|---|---|---|---|---|---|---|---|---|
| KoAT2+MΦRF5+CFR | 24 | 228 | 65 | 11 | 0 | 328 | 4.77 s | 16.40 s |
| KoAT2+MΦRF5+CFRSCC | 24 | 228 | 65 | 11 | 0 | 328 | 5.72 s | 16.53 s |
| KoAT2+CFR | 25 | 216 | 68 | 11 | 0 | 320 | 5.14 s | 11.67 s |
| KoAT2+CFRSCC | 28 | 216 | 66 | 10 | 0 | 320 | 6.00 s | 11.93 s |
| MaxCore | 23 | 214 | 66 | 7 | 0 | 310 | 1.94 s | 5.24 s |
| KoAT2+MΦRF5 | 23 | 204 | 71 | 12 | 0 | 310 | 2.11 s | 5.16 s |
| CFR+KoAT2 | 27 | 200 | 70 | 2 | 1 | 300 | 11.26 s | 19.92 s |
| CFR+KoAT1 | 29 | 187 | 74 | 7 | 0 | 297 | 5.34 s | 12.64 s |
| CoFloCo | 22 | 195 | 66 | 5 | 0 | 288 | 0.81 s | 2.95 s |
| KoAT1 | 25 | 168 | 74 | 12 | 6 | 285 | 2.36 s | 2.97 s |
| KoAT2 | 23 | 176 | 70 | 12 | 0 | 281 | 2.05 s | 2.76 s |
| Loopus | 17 | 169 | 49 | 4 | 0 | 239 | 0.84 s | 0.72 s |