**Templates and Recurrences: Better Together**

*Jason Breck, John Cyphert, Zachary Kincaid, and Thomas Reps*

University of Wisconsin

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(n^{log2(7)}).

(Click here to access the paper: PDF.)