in the CFA). This set of paths is represented by a *path expression* for the vertex $v_8$, which is a regular expression over an alphabet of control flow edges. In principle, this can be accomplished by Kleene’s well-known algorithm for converting a finite automaton into a regular expression [@Kleene1956] (but more efficient algorithms exist [@Tarjan1981]). For example, the following is a path expression for $v_8$: [$${\langle {v^{\textsf{entry}}},v_1 \rangle}\!\cdot\!{\langle v_1,v_2 \rangle}\!\cdot\!\underbrace{\big({\langle v_2,v_3 \rangle}\!\cdot\!{\langle v_3,v_4 \rangle}\!\cdot\!\overbrace{({\langle v_4,v_5 \rangle}\!\cdot\!{\langle v_5,v_6 \rangle}\!\cdot\!{\langle v_6,v_4 \rangle})^*}^{\text{Inner loop}}\!\cdot {\langle v_4,v_7 \rangle}\!\cdot\!{\langle v_7,v_2 \rangle}\big)^*}_{\text{Outer loop}}\!\cdot{\langle v_2,v_8 \rangle}$$ ]{}

Once we have a path expression representing the paths to $v_8$, we compute an over-approximation of the executions to $v_8$ by [*evaluating*]{} the path expression in some abstract domain. The main benefit of this algebraic framework is that an analysis is defined simply by providing an interpretation for each of the regular expression operators (sequencing, choice, and iteration, corresponding to the control structures of structured programs), and then we may rely on a path expression algorithm ([@Kleene1956; @Tarjan1981]) to efficiently “lift” the analysis to programs with arbitrary control flow.

Formally, a program analysis (in the framework of [@Farzan2013]) is defined by an *interpretation*, which consists of a *semantic algebra* and 