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.