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 paperKoAT-2013/*
are the examples from our TACAS'14 paperKoAT-2014/*
are the examples from this paper.
SAS10/*
and c-examples/Rank/*
are the examples from (the evaluation of) the paperT2/*
are the examples from (the evaluation of) the paperc-examples/ABC/*
are the examples from (the evaluation of) the paperc-examples/Loopus/*
are the examples from (the evaluation of) the paperc-examples/SPEED/*
are the examples from (the evaluations of) the paperscosta/*
are the examples from the evaluation of the tool COSTA
with its backend PUBS
, obtained from http://costa.ls.fi.upm.es/pubs/examples.php.
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 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:
(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 A
, B
, and C
.
(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 f(X_{1},...,X_{n})
where (for 1 <= i
<= n
) X_{i}
is the i
th
variable of the program and f
is the start location of the transition.
Each of the target states is given in the form
g(t_{1},...,t_{n})
where (for 1 <= i <=
n
) t_{i}
is the value of the i
th variable
after evaluating the transition and g
is 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.