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.
The full technical report, including a number of extensions to the presented approach, and proofs for all theorems, is available as AIB 2013-12.
FGPSF09/*
are the examples from (the evaluation of) the paperKoAT-2013/*
are the examples from our 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/Rank/*
are the C 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.
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 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:
(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 end states), 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. Each of the end states is given as
f(t_{1},...,t_{n})
where (for 1 <= i <=
n
) t_{i}
is the value of the i
th variable
after evaluating the transition. 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
interpreted with arbitrary integers.