A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis

Details on the Experimental Evaluation

Comparison to the tools KoAT, PUBS and Rank

For comparing our implementation to the state-of-the art in automatic bound analysis and complexity analysis, we use the benchmark (682 examples) and results from the empirical evaluation of "Alternating Runtime and Size Complexity Analysis of Integer Programs" (TACAS, 2014) which can be found here. Since our tool is built for analyzing C programs, we had to obtain C translations for the transition systems processed by KoAT. For the subset of examples taken from the T2 benchmark (449 examples) we use the C translation provided here (the original source code from which the transition systems were generated is not available). From the remaining 233 examples we excluded the 13 RAML programs, because we do not see a meaningful way to compare C translations to functional programs. Of the 37 recursive examples in the benchmark we translated 26 by hand to while programs since they are tail-recursive. The other 11 recursive programs were not analyzed by loopus but form part of the comparison below. For the remaining 197 examples we used a script or hand translation on base of the pseudo code provided in the publications from which they were taken. Our benchmark thus contains 658 C files.

Evaluation on Real-World Code

Amortized Loops

The following loops in the cBench Benchmark have an amortized bound, the line numbers refer to the benchmark version submitted with the paper.

Challenging Loop Classes

Running Loopus

The benchmarks and the version of Loopus that was used for the experimental evaluation are available as an archive here. Installation instructions can be found in the file README.txt which is located in the archive. If you don't have a 32 bit Linux system at hand, you can run virtual box with, e.g., this image (user: ubuntu, password: reverse)