## SPEED: Precise and Efficient Static Estimation of Program
Computational Complexity

### Andrey Breslav

Slides from the talk [pdf]

**Abstract**: Linear invariant generation tools generate loop
invariants for imperative programs in the form of linear arithmetic
expressions. The paper I'm reporting on describes how we can
instrument source code of a program with simple counters (variables
which are incremented or set to zero in certain places) in such a way
that the linear invariants generated for the instrumented program can
be combined automatically to obtain non-linear bounds on program
execution time as functions of the size of the programs input
(classical O(f(n)) kinds of bounds). These bounds may even contain
disjunctive functions such as Max(a, b). This approach avoids dealing
with complicated heap analysis by introducing quantitative functions
on the data structures used. These functions are described by the
user: their semantics is given by equations attached to the methods in
ADT interface of the data structure. As a result, SPEED is capable of
finding precise bounds for algorithms on various data structures, such
as StringBuffers or BitVectors, written in C++ and taken for
Microsoft's production code.

**Main references:**

Varmo Vene

Last update 1 April 2010