$\langle [1],[4,5],[6],[8,9]\rangle$, are not spurious. This is consistent with the fact that $\sigma$ actually is not a spurious path. Likewise, ${\mathcal{A}}'$ can be further simplified to the abstract system ${\mathcal{A}}''$ where the blocks $[6]$ and $[7]$ are merged into a new abstract state $[6,7]$. This transformation also keeps examples because now there is no spurious path in ${\mathcal{A}}''$. Let us also notice that if ${\mathcal{A}}$ would get simplified to an abstract system ${\mathcal{A}}'''$ by merging the blocks $[1]$ and $[2,3]$ into a new abstract state $[1,2,3]$ then this transform would not keep examples because we would obtain the spurious loop path $\tau = \langle [1,2,3], [1,2,3], [1,2,3], ... \rangle$ in ${\mathcal{A}}'''$ (because in ${\mathcal{A}}'''$ $[1,2,3]$ has a self-loop) while there is no corresponding spurious abstract path in ${\mathcal{A}}$ whose abstraction in ${\mathcal{A}}'''$ is $\tau$.

EGAS is formalized within the standard abstract interpretation framework by Cousot and Cousot [@CC77; @CC79]. This ensures that EGAS can be applied both in abstract model checking and in abstract interpretation. Consider for instance the following two basic abstract domains $A_1$ and $A_2$ for sign analysis of an integer variable, so that sets of integer numbers in $\wp(\mathbb{Z})$ is the concrete domain.

(0,0) node\[name=2\] [[$0$]{}]{}; (-1,1) 