found for the outer loop and their closed forms are shown to the right (again, with “uninteresting” recurrences omitted). We note that our algorithm extracts these recurrences from ${\varphi}_{\textsf{outer}}$ using only semantic operations: the fact that ${\varphi}_{\textsf{outer}}$ is an abstraction of a looping computation is completely transparent to the analysis. Using the closed forms of the recurrences to the right, we compute the following transition formula for the outer loop:

$$\begin{aligned}
  \varphi_{\textsf{outer}}^{\ostar}&=  {\fbox{$\exists k. k \geq 0 \land q' = q + k \land r' = r - ky \land {\mathit{stable}}(\{x, y\})$}}\\
  &= {\fbox{$q' \geq q \land r' = r - (q'-q)y \land {\mathit{stable}}(\{x, y\})$}}\end{aligned}$$

Finally, we compute a transition formula which approximates all executions which end at $v_8$ as follows: $$\begin{aligned}
  \varphi_P &= {\llbracket {\langle {v^{\textsf{entry}}},v_1 \rangle}\cdot{\langle v_1,v_2 \rangle} \rrbracket} {\odot}\varphi_{\textsf{outer}}^{\ostar}{\odot}{\llbracket {\langle v_2,v_8 \rangle} \rrbracket}\\
  &= {\fbox{$q' \geq 0 \land r' = x - q'y \land r \leq y \land {\mathit{stable}}(\{x, y\})$}}\end{aligned}$$

This formula is strong enough to imply that assertion $x' = q'*y'+r'$ holds at $v_8$. This is particularly interesting because it requires proving a *non-linear* transition invariant for the loop, which is out of scope for many state-of-the-art program analyzers.

Abstracting Loops with Linear Recurrence Analysis {#sec:lra}
