Templates and Recurrences: Better Together
Jason Breck, John Cyphert, Zachary Kincaid, and Thomas Reps
This paper is the confluence of two streams of ideas in the
literature on generating numerical invariants, namely:
(1) template-based methods, and (2) recurrence-based methods.
A template-based method begins with a template that contains
unknown quantities, and finds invariants that match the template by
extracting and solving constraints on the unknowns.
A disadvantage of template-based methods is that they require fixing the set of
terms that may appear in an invariant in advance. This disadvantage is
particularly prominent for non-linear invariant generation,
because the user must supply maximum degrees on polynomials, bases for exponents, etc.
On the other hand, recurrence-based methods are able to find
sophisticated non-linear mathematical relations, including polynomials,
exponentials, and logarithms, because such relations arise as the solutions to
recurrences.
However, a disadvantage of past recurrence-based invariant-generation methods
is that they are primarily loop-based analyses: they use recurrences to relate
the pre-state and post-state of a loop, so it is not obvious how to apply them
to a recursive procedure, especially if the procedure is
non-linearly recursive (e.g., a tree-traversal algorithm).
In this paper, we combine these two approaches and obtain a technique that uses
templates in which the unknowns are functions rather than numbers, and
the constraints on the unknowns are recurrences. The technique
synthesizes invariants involving polynomials, exponentials, and logarithms,
even in the presence of arbitrary control-flow, including any combination of
loops, branches, and (possibly non-linear) recursion.
For instance, it is able to show that
(i) the time taken by merge-sort is O(n log(n)), and
(ii) the time taken by Strassen's algorithm is
O(nlog2(7)).
(Click here to access the paper:
PDF.)
University of Wisconsin