for futher research on recurrence analysis.

We implemented linear recurrence analysis and used it to verify assertions for a suite of benchmarks. Linear recurrence analysis is able to prove the correctness of more benchmarks in this suite than any of the leading verification tools for integer programs.

Overview {#sec:motivation}
========

We will adopt a simple intraprocedural model in which a program is represented by a control flow automaton (CFA) where edges are labeled by program statements. Figure \[fig:example\] depicts such a CFA for a program which computes the quotient and remainder of division of a variable [x]{} by a variable [y]{}. We use this model for the sake of simplicity and to help keep the presentation of our analysis short and self-contained. We hope that the basic idea behind the extension to procedures (implemented in the tool), using the analysis to compute procedure summaries [@Sharir1981], is clear without formal explanation.

Our analysis, linear recurrence analysis (LRA), is presented in the algebraic framework described in [@Farzan2013]. Suppose that we wish to prove that the assertion `assert(x = q*y + r)` always succeeds. We begin by computing the set of paths from ${v^{\textsf{entry}}}$ to $v_8$ (the location corresponding to the [assert]{} statement 