a control flow automaton to its interpretation as a transition formula. For example (again, considering Figure \[fig:example\]), we have $$\begin{aligned}
  {\llbracket {\langle {v^{\textsf{entry}}},v_1 \rangle} \rrbracket} &= {\fbox{$r' = x \land {\mathit{stable}}(\{q, t, x, y\})$}}\\
  {\llbracket {\langle v_1,v_2 \rangle} \rrbracket} &= {\fbox{$q' = 0 \land {\mathit{stable}}(\{r, t, x, y\})$}}\\
  {\llbracket {\langle v_2,v_3 \rangle} \rrbracket} &= {\fbox{$r > y \land {\mathit{stable}}(\{q, r, t, x, y\})$}}\end{aligned}$$ where for $X \subseteq {\textsf{Var}}$, we have ${\mathit{stable}}(X) {\triangleq}{\fbox{$\bigwedge_{x
    \in X} x' = x$}}$; we use this to factor out equalities from the formulas and make them more legible. Boxes around formulas have no meaning, and are used only to make it easier to distinguish between equalities in formulas and the meta-language.

#### **LRA Operators.**

The sequencing and choice operators of our analysis are defined as follows: $$\begin{aligned}
  \varphi {\odot}\psi &= \exists x''. \varphi[x''/x'] \land \psi[x''/x] &
  \text{Sequencing}\\ \varphi {\oplus}\psi &= \varphi \lor \psi & \text{Choice}\end{aligned}$$ (where $\varphi[x''/x']$ denotes $\varphi$ with each primed variable $x'$ replaced by its double-primed counterpart $x''$, and $\psi[x''/x]$ similarly replaces unprimed variables with double-primed variables).

The semantic function, sequencing, and choice operators are sufficient to analyze loop-free code. For example, we may consider how LRA computes a transition invariant for the body 