the *exact* behaviour of a (necessarily) limited class loops, e.g. loops where the body is a sequence of affine assignments (see Section \[sec:relwork\] for a discussion of related literature). We shift the goal to computing *over-approximate* behaviour of *arbitrary* loops. The main novelty of our approach is to make synergistic use of recurrence analysis and compositionality: on one hand, recurrence analysis can be used to compute accurate transition formulas for loops; on the other hand, transition formulas for loop *bodies* can be mined for recurrence relations to enable recurrence analysis.

Compositionality enables using recurrence analysis for arbitrary loops in two ways. First, the fact that the transition formula for a loop is computed from a transition formula for its body makes the control structure of the loop irrelevant (e.g., whether it is a sequence of assignments or contains branching or nested loops – its transition formula is just a formula). Second, having access to a loop body formula when computing a loop summary opens the door to using Satisfiability Modulo Theories (SMT) solvers to extract a broad range *semantic* recurrences. In particular, our analysis is able to exploit *approximate recurrences* (inequations over linear terms) to compute interesting loop invariants even 