This page contains additional information on our article “Automatic Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops”. 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 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 *twn-release* can be downloaded here.
A web-interface using the *twn-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_C_Integer**(CINT) consists of 484 C programs on integers. - The second set
**Complexity_ITS**(CITS) consists of 781 integer programs.

These sets contain almost only examples with linear arithmetic (only 10 examples in **Complexity_C_Integer** and 20 examples in **Complexity_ITS** have non-linear arithmetic). On both collections **Complexity_C_Integer** and **Complexity_ITS**, the existing tools already infer finite runtimes for more than 89 % of those examples that might terminate.

The main benefit of our new integration of the twn-technique is that in this
way one can also infer finite runtime bounds for programs that contain non-linear guards or updates. To demonstrate this, we extended both collections by 20 new examples that represent typical (almost only) non-linear programs, including several
benchmarks from the literature.
For detailed information about the new examples *click* on the respective links.

The two benchmark sets **Complexity_C_Non_Linear** and **Complexity_ITS_Non_Linear** are similar but they differ slightly, as an update of an integer program is performed simultaneously on all variables, whereas in a C program each variable is updated individually.
Additionally, we often made non-deterministic branching in an integer program explicit by slightly changing the control-flow.

- The first set
**Complexity_C_Non_Linear**(see here) consists of 20 C programs. - The second set
**Complexity_ITS_Non_Linear**(see here) consists of 20 integer programs.

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 48 GB of RAM.
The benchmarks were evaluated in parallel such that at most 8 containers were running at once, each limited to 1.9 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.

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 **Complexity_C_Non_Linear**), and MaxCore with CoFloCo as its backend (only evaluated on **Complexity_C_Integer** and **Complexity_C_Non_Linear**).

A timeout of 5 minutes was enforced for every tool and program.

**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 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. For example, the detailed results show that KoAT1 infers an exponential runtime for 6 benchmarks, whereas KoAT2 is able to infer a polynomial bound for 5 of these benchmarks. 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 Successful Runs |
Avg. Runtime on All Runs |
---|---|---|---|---|---|---|---|---|

KoAT2 + TWN + MΦRF5 | 26 | 226 | 68 | 9 | 0 | 329 | 8.66 s | 23.91 s |

KoAT2 + MΦRF5 | 24 | 225 | 68 | 10 | 0 | 327 | 8.25 s | 21.49 s |

KoAT2 + TWN + RF | 27 | 222 | 68 | 9 | 0 | 326 | 8.18 s | 19.69 s |

KoAT2 + RF | 25 | 213 | 68 | 10 | 1 | 317 | 8.51 s | 16.23 s |

MaxCore | 23 | 214 | 66 | 7 | 0 | 310 | 2.02 s | 5.33 s |

CoFloCo | 22 | 195 | 66 | 5 | 0 | 288 | 0.62 s | 2.74 s |

KoAT1 | 25 | 168 | 74 | 12 | 6 | 285 | 1.77 s | 2.60 s |

Loopus | 17 | 169 | 49 | 4 | 0 | 239 | 0.42 s | 0.43 s |

KoAT2 + TWN | 19 | 107 | 1 | 0 | 0 | 127 | 2.50 s | 27.04 s |

**Complexity_C_Non_Linear**

The programs of this benchmark set are again C programs on integer values. Thus, the details on the tools are the same as above.

Again, please *click* on the tool names to obtain a detailed list of all results or to download the output of the corresponding configuration.

All benchmarks can be viewed here.

Tool |
O(1) |
O(n) |
O(n²) |
O(nᵏ), k>2 |
O(EXP) |
< ∞ |
Avg. Runtime on Successful Runs |
Avg. Runtime on All Runs |
---|---|---|---|---|---|---|---|---|

KoAT2 + TWN + RF | 0 | 5 | 5 | 4 | 1 | 15 | 6.75 s | 21.73 s |

KoAT2 + TWN + MΦRF5 | 0 | 5 | 5 | 4 | 1 | 15 | 9.92 s | 24.51 s |

KoAT2 + TWN | 1 | 4 | 2 | 2 | 0 | 9 | 3.14 s | 15.86 s |

MaxCore | 0 | 2 | 0 | 0 | 0 | 2 | 0.59 s | 4.83 s |

Loopus | 0 | 1 | 0 | 1 | 0 | 2 | 0.48 s | 0.49 s |

KoAT1 | 0 | 1 | 0 | 0 | 0 | 1 | 0.38 s | 6.78 s |

CoFloCo | 0 | 1 | 0 | 0 | 0 | 1 | 0.56 s | 0.64 s |

KoAT2 + MΦRF5 | 0 | 1 | 0 | 0 | 0 | 1 | 0.73 s | 24.90 s |

KoAT2 + RF | 0 | 1 | 0 | 0 | 0 | 1 | 1.71 s | 24.51 s |

Note that there is one example where the twn-technique can infer a constant bound, whereas ranking functions infer a linear bound. This constant bound is only detected by the configuration KoAT2 + TWN (which does not use any ranking functions). The other configurations of KoAT2 that feature TWN always apply ranking functions first, and they only use TWN on transitions where ranking functions could not infer any bound. Thus, they can only prove a linear bound for this example.

**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 again used the corresponding configuration from the Termination and Complexity Competition 2019. We do not evaluate MaxCore and Loopus on these benchmarks, as these tools cannot handle integer transitions systems.

Please *click* on the tool names to obtain a detailed list of all results or to download the output of the corresponding configuration. For all configurations of KoAT2, the integer programs in the output have again been rendered as graphs using Graphviz.

Tool |
O(1) |
O(n) |
O(n²) |
O(nᵏ), k>2 |
O(EXP) |
< ∞ |
Avg. Runtime on Successful Runs |
Avg. Runtime on All Runs |
---|---|---|---|---|---|---|---|---|

KoAT2 + TWN + MΦRF5 | 135 | 254 | 97 | 13 | 6 | 505 | 6.89 s | 33.51 s |

KoAT2 + TWN + RF | 135 | 253 | 98 | 12 | 6 | 504 | 6.93 s | 28.49 s |

KoAT2 + MΦRF5 | 134 | 252 | 98 | 13 | 6 | 503 | 6.34 s | 31.95 s |

KoAT2 + RF | 134 | 242 | 97 | 10 | 6 | 489 | 6.54 s | 26.13 s |

KoAT1 | 132 | 214 | 104 | 14 | 5 | 469 | 0.66 s | 9.19 s |

CoFloCo | 126 | 231 | 95 | 9 | 0 | 461 | 3.48 s | 18.45 s |

KoAT2 + TWN | 89 | 132 | 2 | 0 | 4 | 227 | 3.62 s | 32.25 s |

**Complexity_ITS_Non_Linear**

The programs of this benchmark set are again integer programs. Thus, the details on the tools are the same as above.

Again, please *click* on the tool names to obtain a detailed list of all results or to download the output of the corresponding configuration.

All benchmarks can be viewed here.

Tool |
O(1) |
O(n) |
O(n²) |
O(nᵏ), k>2 |
O(EXP) |
< ∞ |
Avg. Runtime on Successful Runs |
Avg. Runtime on All Runs |
---|---|---|---|---|---|---|---|---|

KoAT2 + TWN + RF | 0 | 5 | 5 | 4 | 1 | 15 | 2.91 s | 2.94 s |

KoAT2 + TWN + MΦRF5 | 0 | 5 | 5 | 4 | 1 | 15 | 3.02 s | 3.09 s |

KoAT2 + TWN | 1 | 4 | 2 | 2 | 0 | 9 | 1.61 s | 2.96 s |

KoAT1 | 0 | 1 | 0 | 0 | 0 | 1 | 0.38 s | 0.98 s |

CoFloCo | 0 | 1 | 0 | 0 | 0 | 1 | 0.43 s | 0.61 s |

KoAT2 + RF | 0 | 1 | 0 | 0 | 0 | 1 | 0.79 s | 3.05 s |

KoAT2 + MΦRF5 | 0 | 1 | 0 | 0 | 0 | 1 | 0.92 s | 3.55 s |