for numerical invariant generation which, despite loss of contextual information, compares favourably with leading (non-compositional) verification techniques.

The analysis proposed in this paper aims to compute a *transition relation* which over-approximates the behaviour of a given program. The use of transition relations in compositional analysis (e.g., [@Muller-Olm2004; @Popeea2006; @Ammarguellat1990; @Monniaux2009; @Kroening2008; @Biallas2012]) stems from the fact that they can be composed: for example, consider a program $P = P_1;P_2$ which consists of two sub-programs $P_1$ and $P_2$ which are executed in sequence. A transition invariant ${\llbracket P \rrbracket}$ for $P$ can be computed by computing transition invariants ${\llbracket P_1 \rrbracket}$ and ${\llbracket P_2 \rrbracket}$ for the subprograms and then taking ${\llbracket P \rrbracket}$ to be the relational composition: ${\llbracket P \rrbracket} = \{ (s,s'') : \exists s'. (s,s') \in {\llbracket P_1 \rrbracket} \land (s',s'') \in
{\llbracket P_2 \rrbracket} \}.$

A crucial question is how to compute abstractions of loops (i.e., *loop summaries* [@Kroening2008]). Our analysis is based on a classical idea: find recurrence relations for variables modified in the body of a loop, and then use the closed forms for these recurrences as the abstraction of the loop. The focus of research on recurrence analysis has mainly been on computing 