for variables which do not satisfy recurrence equations in the classical sense, thus extending the applicability of recurrence-based invariant generation and overcoming a major barrier in its practical use.

In summary, this paper presents a compositional method for generating numerical invariants (polynomial inequalities of unbounded degree among integer and rational variables) for programs. The main technical contributions are as follows.

We give a method for computing abstractions of loops using summaries for their bodies. This allows our analysis to apply to arbitrary code (with nested loops, unstructured loops, and arbitrary branching). It also makes it possible to use SMT solvers to extract *semantic* recurrence relations rather than syntactic recurrences obtained by pattern-matching source code.

We identify a class recurrence (in)equations that can be efficiently extracted from loop bodies using SMT solving technology and solved using simple linear algebra.

We give a *linearization* algorithm which enables tractable (but necessarily approximate) reasoning about non-linear formulas over rationals and integers (Section \[sec:discussion\]).

We collect ideas from a diverse range of sources (including algebraic program analysis [@Farzan2013], recurrence analysis [@Ammarguellat1990; @Kovacs2008; @Ancourt2010], linearization [@Mine2006], and symbolic abstraction [@Reps2004; @Monniaux2010; @Li2014]), and synthesize them into a cohesive presentation which can be used as a foundation 