Empirical Evaluation of: Alternating Runtime and Size Complexity Analysis of Integer Programs

We present a modular approach to automatic complexity analysis. Based on a novel alternation between finding symbolic time bounds for program parts and using these to infer size bounds on program variables, we can restrict each analysis step to a small part of the program while maintaining a high level of precision. Extensive experiments with the implementation of our method demonstrate its performance and power in comparison with other tools.

Technical report

The full technical report, including a number of extensions to the presented approach, and proofs for all theorems, is available as AIB 2013-12.

Experimental evaluation

Our detailed experimental evaluation is on a second page.

The example set

For the evaluation, we collected the following example sets: You can download the examples, sorted according to their origin, here.

Our implementation KoAT

Installing and using KoAT

The supplied version of KoAT is compiled for 32bit Linux on Intel x86. To use it, you need a version of Yices 1, installed as a binary named yices in a directory contained in your $PATH.

Additionally, install KoAT (file koat) in a directory contained in your $PATH.

To run KoAT on an example file test.koat execute the command $ koat test.koat. The proof attempt is then printed on the screen.

We saved the factSum Example from above in the file sect4-facSum.koat.

Running KoAT on this example is then achieved in the following way: 

$ koat sect4-facSum.koat
YES(?, 105*b + 11*b^2 + 56)

Initial complexity problem:
1:      T:
                (1, 1)    l0(a, b) -> Com_1(l1(0, b))
                (?, 1)    l1(a, b) -> Com_2(l2(a, b), l3(a, b)) [ b >= 0 ]
                (?, 1)    l1(a, b) -> Com_1(l4(a, b)) [ 0 >= b + 1 ]
.
.
.
                (11*b^2 + 17*b + 6, 1)    l8(a, b) -> Com_1(l8(c, b - 1)) [ b >= 1 ]
        start location:
                l0

Complexity upper bound 105*b + 11*b^2 + 56

Time: 0.377 sec (SMT: 0.350 sec)

The input format for KoAT

The input of KoAT is stored in text files with the extension .koat. To see examples of such files, consider the provided collection of examples. The format is an extension of the file format used in the Termination Competition.

As an example, consider the encoding of the program factSum from Appendix A.1 (Recursion) of our paper: 

(GOAL COMPLEXITY)
(STARTTERM (FUNCTIONSYMBOLS l0))
(VAR A B C)
(RULES
  l0(A,B) -> Com_1(l1(0,B))
  l1(A,B) -> Com_2(l2(A,B),l3(A,B)) :|: B >= 0
  l1(A,B) -> Com_1(l4(A,B)) :|: 0 >= B + 1
  l2(A,B) -> Com_1(l1(C,B - 1)) :|: B >= 0
  l3(A,B) -> Com_1(l5(C,B))
  l5(A,B) -> Com_1(l6(1,B))
  l6(A,B) -> Com_2(l7(A,B),l8(A,B)) :|: B >= 1
  l6(A,B) -> Com_1(l9(A,B)) :|: 0 >= B
  l7(A,B) -> Com_1(l9(C,B))
  l8(A,B) -> Com_1(l8(C,B - 1)) :|: B >= 1
)

Each file consists of four parts: