Empirical Evaluation of: Analyzing Runtime and Size Complexity of Integer Programs

We present a modular approach to automatic complexity analysis of integer programs. Based on a novel alternation between finding symbolic time bounds for program parts and using these to infer bounds on the sizes of program variables, we can restrict each analysis step to a small part of the program while maintaining a high level of precision. The bounds computed by our method are polynomial or exponential expressions that depend on the absolute values of input parameters.

We show how to extend our approach to arbitrary cost measures, allowing to use our technique to find upper bounds for other expended resources, such as network requests or energy consumption. Our contributions are implemented in the open source tool KoAT, and extensive experiments show the performance and power of our implementation in comparison with other tools.

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 find all examples, as well as our tool, on github.

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

For example, the facSum example from Sect. 5.1 of our paper is stored 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 Sect. 5.1 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: