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.
FGPSF09/*are the examples from (the evaluation of) the paper
KoAT-2013/*are the examples from our TACAS'14 paper
KoAT-2014/*are the examples from this paper.
c-examples/Rank/*are the examples from (the evaluation of) the paper
T2/*are the examples from (the evaluation of) the paper
c-examples/ABC/*are the examples from (the evaluation of) the paper
c-examples/Loopus/*are the examples from (the evaluation of) the paper
c-examples/SPEED/*are the examples from (the evaluations of) the papers
costa/*are the examples from the evaluation of the tool
COSTAwith its backend
PUBS, obtained from http://costa.ls.fi.upm.es/pubs/examples.php.
To run KoAT on an example file
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
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 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
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:
(GOAL COMPLEXITY), specifying that the goal of this file is complexity analysis.
(STARTTERM (FUNCTIONSYMBOLS start)). Currently, only one state (here start) may be specified as a start state.
(VAR A B C)declares the variables
(RULES ...). Each transition consists of a start state, an arrow (
->), a list of end states (wrapped in
Com_k(...), where k is the number of target states of the transition), and an optional constraint separated by
:|:from the rest of the state. The start state is given in the form
1 <= i <= n)
ith variable of the program and
fis the start location of the transition. Each of the target states is given in the form
1 <= i <= n)
tiis the value of the
ith variable after evaluating the transition and
gis a target location. All values and constraints have to be given as polynomials over the variables in the
(VAR ...)section. Variables not occurring in the start state are instantiated with arbitrary integers.