LARA

Equivalent Form of Abstract Interpretation Function

Instead of computing the sequence $(F^{\#})^n(\bot)$ for

\begin{equation*}
   F^{\#}(g^{\#})(p_2) = init(p_2) \sqcup g^{\#}(p_2) \sqcup \bigsqcup_{(p_1,p_2) \in E} 
     sp^{\#}(g^{\#}(p_1),r(p_1,p_2))
\end{equation*}

we can just as well compute the sequence $(F_0^{\#})^n(\bot)$ where we omit the old values:

\begin{equation*}
   F_0^{\#}(g^{\#})(p_2) = init(p_2) \sqcup \bigsqcup_{(p_1,p_2) \in E} 
     sp^{\#}(g^{\#}(p_1),r(p_1,p_2))
\end{equation*}

(In both cases we also include the initial set of states for the entry program point, they can be represented as special incoming edges.)

Lemma: Function $F_0^{\#}$ is monotonic and

\begin{equation*}
   (F_0^{\#})^n(\bot) = (F^{\#})^n(\bot)
\end{equation*}

Proof: