---
abstract: 'In static analysis, approximation is typically encoded by abstract domains, providing systematic guidelines for specifying approximate semantic functions and precision assessments. However, it may happen that an abstract domain contains redundant information for the specific purpose of approximating a given semantic function modeling some behavior of a system. This paper introduces correctness kernels of abstract interpretations, a methodology for simplifying abstract domains, i.e.removing abstract values from them, in a maximal way while retaining exactly the same approximate behavior of the system under analysis. We show that, in abstract model checking and predicate abstraction, correctness kernels provide a simplification paradigm of the abstract state space that is guided by examples, meaning that it preserves spuriousness of examples (i.e., abstract paths). In particular, we show how correctness kernels can be integrated with the well-known CEGAR (CounterExample-Guided Abstraction Refinement) methodology.'
author:
- '[Roberto Giacobazzi       Francesco Ranzato]{}'
title: Correctness Kernels of Abstract Interpretations
---

Introduction {#intro}
============

In static analysis and verification, model-driven *abstraction refinement* has emerged in the last decade as a fundamental method for improving abstractions towards more precise yet efficient analyses. The basic idea is simple: given an abstraction modeling some observational behavior of the system to analyze, refine the abstraction in order to remove the artificial computations that may appear in the approximate analysis by considering how the concrete system behaves when false alarms or spurious traces are encountered. The general concept of using spurious counterexamples for refining an abstraction stems from the CounterExample-Guided Abstraction Refinement (CEGAR) paradigm [@cgjlv00; @cgjlv03]. The model here drives the automatic identification of prefixes of the counterexample path that do not correspond to an actual trace in the concrete model, by isolating abstract (failure) states that need to be refined in order to eliminate that spurious counterexample. Model-driven refinements, such as CEGAR, provide algorithmic methods for achieving abstractions that are complete (i.e., precise [@gq01; @grs00]) with respect to some given property of the concrete model.

We investigate here the dual problem of *abstraction simplification*. Instead of refining abstractions in order to eliminate spurious traces, our goal is to simplify an abstraction $A$ towards a simpler (ideally, the simplest) model $A_s$ that maintains the same approximate behavior as $A$ does. In abstract model checking, this abstraction simplification has *to keep the same examples* of the concrete system in the following sense. Recall that an abstract path $\pi$ in an abstract transition system ${\mathcal{A}}$ is *spurious* when no real concrete path is abstracted to $\pi$. Assume that a given abstract state space $A$ of a system ${\mathcal{A}}$ gets simplified to $A_s$ and thus gives rise to a more abstract system ${\mathcal{A}}_s$. Then, we say that ${\mathcal{A}}_s$ keeps the same examples of ${\mathcal{A}}$ when the following condition is satisfied: if $\pi_{A_s}$ is a spurious path in the simplified abstract system ${\mathcal{A}}_s$ then there exists a spurious path $\pi_A$ in the original system ${\mathcal{A}}$ that is abstracted to $\pi_{A_s}$. Such a methodology is called EGAS, Example-Guided Abstraction Simplification, since this abstraction simplification does not add spurious paths, namely, it does keep examples, since each spurious path in ${\mathcal{A}}_s$ comes as an abstraction of a spurious path in ${\mathcal{A}}$.

=\[-&gt;,&gt;=latex’\] (0,2) node\[name=1\][1]{} (2,5) node\[name=2\][2]{} (2,3) node\[name=3\][3]{} (2,1) node\[name=4\][4]{} (2,-1) node\[name=5\][5]{} (4,3) node\[name=6\][6]{} (4,1) node\[name=7\][7]{} (6,3) node\[name=8\][8]{} (6,1) node\[name=9\][9]{}; (8,2) node\[name=f\][$\Rightarrow$]{}; (0,5) node\[name=a\][$\mathcal{A}$]{}; (1) to (2); (1) to (4); (2) to (6); (3) to (7); (4) to (6); (5) to (7); (6) to (8); (7) to (9);

(1.north west) ++(-0.1,0.1) node\[name=a1\] (1.south east) ++(0.1,-0.1) node\[name=a2\]; (a1) rectangle (a2);

(2.north west) ++(-0.1,0.1) node\[name=b1\] (3.south east) ++(0.1,-0.1) node\[name=b2\]; (b1) rectangle (b2);

(4.north west) ++(-0.1,0.1) node\[name=b3\] (5.south east) ++(0.1,-0.1) node\[name=b4\]; (b3) rectangle (b4);

(6.north west) ++(-0.1,0.1) node\[name=c1\] (6.south east) ++(0.1,-0.1) node\[name=c2\]; (c1) rectangle (c2);

(7.north west) ++(-0.1,0.1) node\[name=c3\] (7.south east) ++(0.1,-0.1) node\[name=c4\]; (c3) rectangle (c4);

(8.north west) ++(-0.1,0.1) node\[name=d1\] (9.south east) ++(0.1,-0.1) node\[name=d2\]; (d1) rectangle (d2);

(10,2) node\[name=1\][1]{} (12,5) node\[name=2\][2]{} (12,3) node\[name=3\][3]{} (12,1) node\[name=4\][4]{} (12,-1) node\[name=5\][5]{} (14,3) node\[name=6\][6]{} (14,1) node\[name=7\][7]{} (16,3) node\[name=8\][8]{} (16,1) node\[name=9\][9]{}; (18,2) node\[name=f\][$\Rightarrow$]{}; (10,5) node\[name=a\][$\mathcal{A}'$]{}; (1) to (2); (1) to (4); (2) to (6); (3) to (7); (4) to (6); (5) to (7); (6) to (8); (7) to (9);

(1.north west) ++(-0.1,0.1) node\[name=a1\] (1.south east) ++(0.1,-0.1) node\[name=a2\]; (a1) rectangle (a2);

(2.north west) ++(-0.1,0.1) node\[name=b1\] (5.south east) ++(0.1,-0.1) node\[name=b2\]; (b1) rectangle (b2);

(6.north west) ++(-0.1,0.1) node\[name=c1\] (6.south east) ++(0.1,-0.1) node\[name=c2\]; (c1) rectangle (c2);

(7.north west) ++(-0.1,0.1) node\[name=c3\] (7.south east) ++(0.1,-0.1) node\[name=c4\]; (c3) rectangle (c4);

(8.north west) ++(-0.1,0.1) node\[name=d1\] (9.south east) ++(0.1,-0.1) node\[name=d2\]; (d1) rectangle (d2);

(20,2) node\[name=1\][1]{} (22,5) node\[name=2\][2]{} (22,3) node\[name=3\][3]{} (22,1) node\[name=4\][4]{} (22,-1) node\[name=5\][5]{} (24,3) node\[name=6\][6]{} (24,1) node\[name=7\][7]{} (26,3) node\[name=8\][8]{} (26,1) node\[name=9\][9]{};

(20,5) node\[name=a\][$\mathcal{A}''$]{}; (1) to (2); (1) to (4); (2) to (6); (3) to (7); (4) to (6); (5) to (7); (6) to (8); (7) to (9);

(1.north west) ++(-0.1,0.1) node\[name=a1\] (1.south east) ++(0.1,-0.1) node\[name=a2\]; (a1) rectangle (a2);

(2.north west) ++(-0.1,0.1) node\[name=b1\] (5.south east) ++(0.1,-0.1) node\[name=b2\]; (b1) rectangle (b2);

(6.north west) ++(-0.1,0.1) node\[name=c1\] (7.south east) ++(0.1,-0.1) node\[name=c2\]; (c1) rectangle (c2);

(8.north west) ++(-0.1,0.1) node\[name=d1\] (9.south east) ++(0.1,-0.1) node\[name=d2\]; (d1) rectangle (d2);

Let us illustrate how EGAS works through a simple example. Let us consider the abstract transition system ${\mathcal{A}}$ in Figure \[figure-1\], where concrete states are numbers which are abstracted by blocks of the state partition $\{[1],[2,3],[4,5],[6],[7],[8,9]\}$. The abstract state space of ${\mathcal{A}}$ is simplified by merging the abstract states $[2,3]$ and $[4,5]$: EGAS guarantees that this can be safely done because $\operatorname{pre}^\sharp ([2,3]) = \{[1]\}=
\operatorname{pre}^\sharp([4,5])$ and $\operatorname{post}^\sharp ([2,3]) = \{[6],[7]\}=
\operatorname{post}^\sharp([4,5])$, where $\operatorname{pre}^\sharp$ and $\operatorname{post}^\sharp$ denote, respectively, the abstract predecessor and successor functions in ${\mathcal{A}}$. This abstraction simplification leads to the abstract system ${\mathcal{A}}'$ in Figure \[figure-1\]. Let us observe that the abstract path $\pi = \langle [1], [2,3,4,5], [7], [8,9]\rangle$ in ${\mathcal{A}}'$ is spurious because there is no concrete path whose abstraction in ${\mathcal{A}}'$ is $\pi$, while $\pi$ is instead the abstraction of the spurious path $\langle [1],$ $[4,5],$ $[7], [8,9]\rangle$ in ${\mathcal{A}}$. On the other hand, consider the path $\sigma = \langle [1], [2,3,4,5], [6], [8,9]\rangle$ in ${\mathcal{A}}'$ and observe that all the paths in ${\mathcal{A}}$ that are abstracted to $\pi'$, i.e.$\langle [1],[2,3],[6],[8,9]\rangle$ and $\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) node\[name=3\] [[$\mathbb{Z}_{\leq 0}$]{}]{}; (1,1) node\[name=4\] [[$\mathbb{Z}_{\geq 0}$]{}]{}; (0,2) node\[name=5\] [[$\mathbb{Z}$]{}]{};

(-2.5,1) node [[$A_1$]{}]{};

\(2) – (3); (2) – (4); (3) – (5); (4) – (5);

(5,1) node [[$A_2$]{}]{};

(4,0) node\[name=2\] [[$\mathbb{Z}_{\geq 0}$]{}]{}; (4,2) node\[name=5\] [[$\mathbb{Z}$]{}]{};

\(2) – (5);

Recall that in abstract interpretation the best correct approximation of a semantic function $f$ on an abstract domain $A$ that is defined through abstraction/concretization maps $\alpha$/$\gamma$ is given by $f^A {\triangleq}\alpha \circ f \circ \gamma$. Consider a simple operation of increment $x$++ on an integer variable $x$. In this case, the best correct approximations on $A_1$ and $A_2$ are as follows: $$\begin{gathered}
\text{++}^{A_1} = \{0 \mapsto \mathbb{Z}_{\geq 0},\: 
\mathbb{Z}_{\leq 0} \mapsto \mathbb{Z},\: 
\mathbb{Z}_{\geq 0} \mapsto \mathbb{Z}_{\geq 0},\: 
\mathbb{Z} \mapsto \mathbb{Z}\},\\[-2.5pt]
\text{++}^{A_2} = \{
\mathbb{Z}_{\geq 0} \mapsto \mathbb{Z}_{\geq 0},\: 
\mathbb{Z} \mapsto \mathbb{Z}\}.\end{gathered}$$ We observe that the best correct approximations of $\text{++}$ in $A_1$ and $A_2$ encode the same function, meaning that the approximations of $\text{++}$ in $A_1$ and $A_2$ are equivalent, the latter being clearly simpler. In fact, we have that $\gamma_{A_1} \circ \text{++}^{A_1} \circ \alpha_{A_1}$ and $\gamma_{A_2} \circ \text{++}^{A_2} \circ \alpha_{A_2}$ are exactly the same function on $\wp(\mathbb{Z})$. In other terms, the abstract domain $A_1$ contains some “irrelevant” abstract values for approximating the increment operation, that is, $0$ and $\mathbb{Z}_{\leq 0}$. This simplification of an abstract domain relatively to a semantic function is formalized in the most general abstract interpretation setting. This allows us to provide, for generic continuous semantic functions, a systematic and constructive method, that we call *correctness kernel*, for simplifying a given abstraction $A$ relatively to a given semantic function $f$ towards the unique minimal abstract domain that induces an equivalent approximate behavior of $f$ as in $A$. We show how correctness kernels can be embedded within the CEGAR methodology by providing a novel refinement heuristics in a CEGAR iteration step which turns out to be more accurate than the basic refinement heuristics [@cgjlv03]. We also describe how correctness kernels may be applied in predicate abstraction-based model checking [@ddp99; @gs97] for reducing the search space without applying Ball et al.’s [@bpr03] Cartesian abstractions, which typically yield additional loss of precision.

This is an extended and revised version of the conference paper [@gr10] that includes full proofs.

Correctness Kernels
===================

As usual in standard abstract interpretation [@CC77; @CC79], abstract domains (or abstractions) are specified by Galois connections/insertions (GCs/GIs for short) or, equivalently, adjunctions. Concrete and abstract domains, $\tuple{C,\leq_C}$ and $\tuple{A,\leq_A}$, are assumed to be complete lattices which are related by abstraction and concretization maps $\alpha:C{\rightarrow}A$ and $\gamma:A {\rightarrow}C$ that give rise to an adjunction $(\alpha,C,A,\gamma)$, that is, for all $a$ and $c$, $\alpha(c) \leq_A a {\Leftrightarrow}c \leq_C \gamma(a)$. It is known that $\ok{\mu_A {\triangleq}\gamma \circ \alpha: C {\rightarrow}C}$ is an upper closure operator (uco) on $C$, i.e. a monotone, idempotent and increasing function. Also, abstract domains can be equivalently defined as ucos, meaning that any GI $(\alpha,C,A,\gamma)$ induces the uco $\mu_A$, any uco $\mu: C{\rightarrow}C$ induces the GI $(\mu, C, \mu(C), \lambda x.x)$, and these two transforms are the inverse of each other. GIs of a common concrete domain $C$ are preordered w.r.t. their relative precision as usual: ${\mathcal{G}}_1 = (\alpha_1,C,A_1,\gamma_1)\sqsubseteq {\mathcal{G}}_2=(\alpha_2,C,A_2,\gamma_2)$ — i.e. $A_1$/$A_2$ is a refinement/simplification of $A_2$/$A_1$ — iff $\gamma_2 (\alpha_2(C)) \subseteq\gamma_1 (\alpha_1 (C))$. Moreover, ${\mathcal{G}}_1$ and ${\mathcal{G}}_2$ are equivalent when ${\mathcal{G}}_1
\sqsubseteq {\mathcal{G}}_2$ and ${\mathcal{G}}_2 \sqsubseteq {\mathcal{G}}_1$. We denote by $\operatorname{Abs}(C)$ the family of abstract domains of $C$ up to the above equivalence. It is well known that $\tuple{\operatorname{Abs}(C),\sqsubseteq}$ is a complete lattice, so that one can consider the most concrete simplification (i.e., lub $\sqcup$) and the most abstract refinement (i.e., glb $\sqcap$) of any family of abstract domains. Let us recall that the lattice of abstract domains $\tuple{\operatorname{Abs}(C),\sqsubseteq}$ is isomorphic to the lattice of ucos on $C$ $\tuple{\operatorname{uco}(C),\sqsubseteq}$, where $\sqsubseteq$ denotes the pointwise ordering between functions, so that lub’s and glb’s of abstractions can be equivalently characterized in $\operatorname{uco}(C)$. Let us also recall that each $\mu\in \operatorname{uco}(C)$ is uniquely determined by its image $\operatorname{img}(\mu)=\mu(C)$ because $\mu = \lambda
x. \wedge \!\{ y\in C~|~ y\in \mu(C), \, x\leq y\}$. Moreover, a subset $X\subseteq C$ is the image of some uco on $C$ iff $X$ is meet-closed, i.e. $X=\ok{\operatorname{Cl}_\wedge 
(X){\triangleq}}\{ \wedge Y~|~ Y\subseteq
X\}$ (note that $\top_C =\wedge \varnothing \in \operatorname{Cl}_\wedge (X)$). Often, we will identify ucos with their images. This does not give rise to ambiguity, since one can distinguish their use as functions or sets according to the context. Hence, if $A,B\in \operatorname{Abs}(C)$ are two abstractions then they can be viewed as images of two ucos on $C$, denoted respectively by $\mu_A$ and $\mu_B$, so that $A$ is more precise than $B$ when $\operatorname{img}(\mu_B) \subseteq \operatorname{img}(\mu_A)$.

Let $f:C{\rightarrow}C$ be some concrete semantic function — for simplicity, we consider 1-ary functions — and let $\ok{f^\sharp:A {\rightarrow}A}$ be a corresponding abstract function defined on some abstraction $A\in \operatorname{Abs}(C)$. Then, $\ok{\tuple{A,f^\sharp}}$ is a sound abstract interpretation when $\ok{\alpha \circ f \sqsubseteq f^\sharp\circ \alpha}$. Moreover, the abstract function $\ok{f^A {\triangleq}\alpha \circ f \circ \gamma: A\rightarrow A}$ is called the *best correct approximation* (b.c.a.) of $f$ on $A$ because any abstract interpretation $\ok{\tuple{A,f^\sharp}}$ is sound iff $\ok{f^A \sqsubseteq f^\sharp}$. Hence, for any abstraction $A$, $\ok{f^A}$ plays the role of the best possible approximation of $f$ on $A$.

The Problem
-----------

Given a semantic function $f:C\rightarrow C$ on some concrete domain $C$ and an abstraction $A \in \operatorname{Abs}(C)$, does there exist the *most abstract domain* that induces the same best correct approximation of $f$ as $A$ does?

Let us formalize the above question. Consider two abstractions $A,B\in \operatorname{Abs}(C)$. We say that $A$ and $B$ induce the same best correct approximation of $f$ when $f^A$ and $f^B$ are the same function up to isomorphic representations of abstract values. If $\mu_A$ and $\mu_B$ are the corresponding ucos then this boils down to: $$\mu_A {\circ}f {\circ}\mu_A = \mu_B {\circ}f {\circ}\mu_B .$$ In order to keep the notation easy, this is denoted simply by $\ok{f^A = f^B}$. Also, if $F\subseteq C{\rightarrow}C$ is a set of concrete functions then $\ok{F^A = F^B}$ means that for any $f\in F$, $\ok{f^A = f^B}$. Hence, given $A\in \operatorname{Abs}(C)$ and by defining $$A_{s} \triangleq \sqcup \{B \in \operatorname{Abs}(C)~|~ F^B = F^A\}$$ the question is whether $F^{A_{s}} = F^A$ holds or not. This leads us to the following notion of correctness kernel.

Given $F\subseteq C{\mbox{\raisebox{0ex}[1ex][1ex]{$
  \mathrel{\mathop{
\hspace*{1pt}\longrightarrow\hspace*{1pt}}\limits^{\,_{\mbox{\tiny
\hspace*{-2.2pt}}}}}$}}} C$ define: $\mathscr{K}_F: \operatorname{Abs}(C) \rightarrow \operatorname{Abs}(C)$ as $$\mathscr{K}_F(A) \triangleq \sqcup \{ B \in \operatorname{Abs}(C) ~|~ F^B = F^A\}.$$ If $F^{\mathscr{K}_F(A)} = F^A$ then $\mathscr{K}_F(A)$ is called the *correctness kernel* of $A$ for $F$.

It is worth remarking that the dual question on the existence of the *most concrete domain* that induces the same best correct approximation of $f$ as $A$ has a negative answer, as shown by the following simple example.

\[esempio2\] Consider the lattice $C$ depicted below.

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

\(1) – (2); (2) – (3); (2) – (4); (3) – (5); (4) – (5);

Let us also consider the monotonic function $f:C\rightarrow C$ defined as $f\triangleq \{1\mapsto 1,\, 2\mapsto 1,\, 3\mapsto 5,\, 4\mapsto 5,\, 5\mapsto 5\}$ and the abstraction $\mu \in \operatorname{uco}(C)$ whose image is $\mu \triangleq \{1,5\}$. Let us observe that $\mu{\circ}f {\circ}\mu = \{1\mapsto 1,\, 2\mapsto 5,\, 3\mapsto 5,\, 4\mapsto 5,\, 5\mapsto 5\}$. Consider now the abstractions $\rho_1 \triangleq \{1,3,5\}$ and $\rho_2 \triangleq \{1,4,5\}$ and observe that $\rho_i {\circ}f {\circ}\rho_i = \mu{\circ}f {\circ}\mu$. However, we have that $\rho_1 \sqcap \rho_2 = \lambda x.x$, because the image of $\rho_1 \sqcap \rho_2$ is ${\mathcal{M}}(\rho_1 \cup \rho_2) = 
\{1,2,3,4,5\}$. Hence, $(\rho_1 \sqcap \rho_2) {\circ}f {\circ}(\rho_1 \sqcap \rho_2) = f \neq \mu{\circ}f {\circ}\mu$. Therefore, if we let $\rho_r = \sqcap \{ \rho \in \operatorname{uco}(C)~|~ \rho \circ f \circ 
 \rho = \mu \circ f \circ \mu\}$ then $\rho_r = \lambda x.x$. Consequently, the most concrete domain that induces the same best correct approximation of $f$ as $\mu$ does not exist.

The Solution
------------

Our key technical result is the following *constructive* characterization of the property of “having the same b.c.a.” for two comparable abstract domains. In the following, given a poset $A$ and any subset $S\subseteq A$, $\max (S) \triangleq \{
x\in S~|~ \forall y\in S.\; x\leq_A y \Rightarrow x = y\}$ denotes the set of maximal elements of $S$ in $A$.

\[key\] Let $f: C\rightarrow C$ and $A,B \in \operatorname{Abs}(C)$ such that $B\subseteq A$. Suppose that $f{\circ}\mu_A : C {\rightarrow}C$ is continuous (i.e., preserves lub’s of chains in $C$). Then, $$\textstyle
f^B = f^A \;{\Leftrightarrow}\; \operatorname{img}(f^A) \cup \bigcup_{y\in A} 
\max(\{x\in A~|~f^A(x) \leq_A y\}) 
\subseteq B.$$

Let $\mu$ and $\rho$ be the ucos induced by, respectively, the abstractions $A$ and $B$, so that $\mu \sqsubseteq \rho$. Then, observe that $\operatorname{img}(f^A) = \mu(f(\mu(C)))$ and $\{x\in A ~|~ f^A(x) \leq_A y\} = (\mu {\circ}f {\circ}\mu)^{-1}(\downarrow \!y)$. We therefore prove the following equivalent statement which is formalized through ucos: $$\rho {\circ}f {\circ}\rho = \mu {\circ}f {\circ}\mu
\text{~~iff~~}
\mu(f(\mu(C))) \cup \textstyle \bigcup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\subseteq \rho.$$ Let us first prove that $$\rho {\circ}f {\circ}\rho = \mu {\circ}f {\circ}\mu \:\Leftrightarrow\: \rho {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\rho\eqno(*)$$\
($\Rightarrow$) On the one hand, $$\begin{aligned}
\mu {\circ}f {\circ}\mu = \rho {\circ}f {\circ}\rho  & \Rightarrow 
\text{~~~~[by applying $\rho$ to both sides]}
\\
\rho {\circ}\mu {\circ}f {\circ}\mu = \rho{\circ}\rho {\circ}f {\circ}\rho 
& \Rightarrow \text{~~~~[because $\rho {\circ}\rho = \rho$ and 
$\rho {\circ}\mu = \rho$]} \\
\rho  {\circ}f {\circ}\mu = \rho {\circ}f {\circ}\rho &\Rightarrow \\
\rho  {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu &\end{aligned}$$ and on the other hand, $$\begin{aligned}
\mu {\circ}f {\circ}\mu = \rho {\circ}f {\circ}\rho  & \Rightarrow 
\text{~~~~[by applying $\rho$ in front to both sides]}
\\
\mu {\circ}f {\circ}\mu {\circ}\rho = \rho{\circ}f {\circ}\rho {\circ}\rho 
& \Rightarrow 
\text{~~~~[because $\rho {\circ}\rho = \rho$ and 
$\mu {\circ}\rho = \rho$]} \\
\mu  {\circ}f {\circ}\rho = \rho {\circ}f {\circ}\rho &\Rightarrow \\
\mu  {\circ}f {\circ}\rho = \mu {\circ}f {\circ}\mu &\end{aligned}$$ so that $\rho {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\rho$.\
($\Leftarrow$) We have that: $$\begin{aligned}
\rho {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\rho & \Rightarrow 
\text{~~~~[by applying $\rho$ to both sides]}
\\
\rho {\circ}\rho {\circ}f {\circ}\mu = \rho {\circ}\mu {\circ}f {\circ}\rho & \Rightarrow \text{~~~~[since $\rho {\circ}\rho = \rho$ and 
$\rho {\circ}\mu = \rho$]}\\
\rho {\circ}f {\circ}\mu = \rho {\circ}f {\circ}\rho & \Rightarrow\\
\mu {\circ}f {\circ}\mu = \rho {\circ}f {\circ}\rho. &\end{aligned}$$

Let us now observe that $\rho {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu$: in fact, since $\rho = \rho {\circ}\mu$, this is equivalent to $\rho {\circ}\mu {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu$, which is obviously equivalent to $\mu (f(\mu(C))) \subseteq \rho$.

Since $\rho = \mu {\circ}\rho$, we have that $\mu {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\rho$ is equivalent to $\mu {\circ}(f {\circ}\mu) = \mu {\circ}(f{\circ}\mu) {\circ}\rho$. By the characterization of completeness in [@grs00 Lemma 4.2], since, by hypothesis, $f {\circ}\mu$ is continuous, we have that the completeness equation $\mu {\circ}(f {\circ}\mu) = \mu {\circ}(f{\circ}\mu) {\circ}\rho$ is equivalent to $\cup_{y\in \mu} \max((f {\circ}\mu)^{-1}(\downarrow\! y))\subseteq \rho$, which is in turn equivalent to $\cup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\subseteq \rho$.

Summing up, we have thus shown that $$\rho {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\mu = \mu {\circ}f {\circ}\rho \:\Leftrightarrow\: \mu (f(\mu(C))) \cup \textstyle 
\bigcup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\subseteq \rho$$ and this, by the above property $(*)$, implies the thesis.

It is important to remark that the above proof basically consists in reducing the equality $f^A = f^B$ between b.c.a.’s to a standard property of completeness of the abstract domains $A$ and $B$ for the function $f$ and then in exploiting the constructive characterization of completeness of abstract domains by Giacobazzi et al. [@grs00 Section 4]. In this sense, the proof itself is particularly interesting because it provides an unexpected reduction of best correct approximations to a completeness problem.

As a consequence of Lemma \[key\] we obtain the following constructive result of existence for correctness kernels. Recall that if $X\subseteq A$ then $\operatorname{Cl}_\wedge (X)$ denotes the glb-closure of $X$ in $A$, while $\operatorname{Cl}_\vee(X)$ denotes the dual lub-closure.

\[kernel\] Let $A \in \operatorname{Abs}(C)$ and $F\subseteq C\rightarrow C$ such that, for any $f\in F$, $f {\circ}\mu_A$ is continuous. Then, the correctness kernel of $A$ for $F$ exists and it is $$\mathscr{K}_F(A) = \operatorname{Cl_\wedge}\Big(\bigcup_{f\in F}\textstyle \operatorname{img}(f^A) \cup  \bigcup_{y\in \operatorname{img}(f^A)} 
\max(\{x\in A~|~f^A(x) = y\})\Big).$$

Let $\mu = \mu_A$. We prove the following equivalent statement formalized through ucos: $\operatorname{Cl_\wedge}\left(\bigcup_{f\in F} \bigcup_{y\in \mu(f(\mu(C)))} \left(\{y\} \cup \max(\{x\in \mu~|~\mu(f(x)) = y\})\right)\right)$ is the correctness kernel of $\mu$ for $F$.

Let $\rho_\mu \triangleq
\operatorname{Cl_\wedge}\left( \mu(f(\mu(C))) \cup \textstyle \bigcup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\right)$. By Lemma \[key\], we have that $\sqcup \{\rho \in \operatorname{uco}(C)~|~ \rho \sqsupseteq \mu,\: 
\rho {\circ}f {\circ}\rho =  \mu {\circ}f {\circ}\mu\} =
\rho_\mu$. Since $\sqcup \{\rho \in \operatorname{uco}(C)~|~ \rho \sqsupseteq \mu,\: 
\rho {\circ}f {\circ}\rho =  \mu {\circ}f {\circ}\mu\} = 
\sqcup \{\rho \in \operatorname{uco}(C)~|~ 
\rho {\circ}f {\circ}\rho =  \mu {\circ}f {\circ}\mu\}$, as a consequence we also have that $\rho_\mu$ is the correctness kernel of $\mu$ for $F$.\
Therefore, let us prove that $$\begin{gathered}
\operatorname{Cl_\wedge}\left( \mu(f(\mu(C))) \cup \cup_{y\in \mu} \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))\right) =\\
\textstyle \operatorname{Cl_\wedge}\left( \bigcup_{f\in F} \bigcup_{y\in \mu(f(\mu(C)))} \left(\{y\} \cup \max(\{x\in \mu~|~\mu(f(x)) = y\})\right) \right).\end{gathered}$$ Let us first observe that for any $y\in \mu$, if $z\in \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))$ then $z\in\mu$: in fact, $\mu(f(\mu(\mu(z)))) = \mu(f(\mu(z))) \leq y$, so that from $z \leq \mu(z)$, by maximality of $z$, we get $z=\mu(z)$.\
$(\subseteq)$: Consider $y\in \mu$ and $z\in  \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))$. Then, it turns out that $z \in \max(\{x\in \mu~|~\mu(f(x)) = \mu(f(\mu(z)))\})$. In fact, since $z=\mu(z)$, we have that $\mu(f(z))=\mu(f(\mu(z)))$. Moreover, if $u\in \{x\in \mu~|~\mu(f(x)) = \mu(f(\mu(z)))\}$ and $z \leq u$ then $\mu(f(\mu(u))) = \mu(f(u)) = 
\mu(f(\mu(z))) \leq y$, so that, by maximality of $z$, $z=u$, i.e., $z\in \max(\{x\in \mu~|~\mu(f(x)) = \mu(f(\mu(z)))\})$.\
$(\supseteq)$: Consider $y=\mu(f(\mu(w)))$ and $z\in \max(\{x\in \mu~|~\mu(f(x)) = y\})$. Then, $\mu(f(\mu(z))) = \mu(f(z)) = y$ so that $z\in (\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y)$. If $u\in (\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y)$ and $z \leq u$ then $\mu(f(\mu(z))) \leq \mu(f(\mu(u))) \leq y=\mu(f(\mu(w)))=\mu(f(\mu(z)))$. Hence, since $z\leq u \leq \mu(u)$ and by maximality of $z$, we have that $z=\mu(u)$, and in turn $z=u$. Thus, $z\in  \max((\mu {\circ}f {\circ}\mu)^{-1}(\downarrow\! y))$.

Consider sets of integers $\tuple{\wp(\mathbb{Z}),\subseteq}$ as concrete domain domain and the square operation ${\ensuremath{\mathit{sq}}}:\wp(\mathbb{Z}) \rightarrow \wp(\mathbb{Z})$ as concrete function, i.e., ${\ensuremath{\mathit{sq}}}(X) \triangleq \{x^2 ~|~ x\in X\}$, which is obviously additive and therefore continuous. Consider the abstract domain $\operatorname{Sign}\in \operatorname{Abs}(\wp(\mathbb{Z})_\subseteq)$, depicted in the following figure, that represents the sign of an integer variable.

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

(-1,1) node\[name=2\] [[$\mathbb{Z}_{<0}$]{}]{}; (0,1) node\[name=3\] [[$0$]{}]{}; (1,1) node\[name=4\] [[$\mathbb{Z}_{>0}$]{}]{};

(-1,2) node\[name=5\] [[$\mathbb{Z}_{\leq 0}$]{}]{}; (0,2) node\[name=6\] [[$\mathbb{Z}_{\neq 0}$]{}]{}; (1,2) node\[name=7\] [[$\mathbb{Z}_{\geq 0}$]{}]{};

(0,3) node\[name=8\] [[$\mathbb{Z}$]{}]{}; (1) – (2); (1) – (3); (1) – (4); (2) – (5); (2) – (6); (3) – (5); (3) – (7); (4) – (6); (4) – (7); (5) – (8); (6) – (8); (7) – (8);

$\operatorname{Sign}$ induces the following best correct approximation of ${\ensuremath{\mathit{sq}}}$: $$\begin{aligned}
{\ensuremath{\mathit{sq}}}^{\operatorname{Sign}} = \{&\varnothing \mapsto \varnothing, \mathbb{Z}_{<0} \mapsto 
\mathbb{Z}_{> 0}, 0 \mapsto 0, \mathbb{Z}_{> 0} \mapsto
\mathbb{Z}_{> 0}, \mathbb{Z}_{\leq 0} \mapsto \mathbb{Z}_{\geq 0}, \\
& \mathbb{Z}_{\neq 0} \mapsto \mathbb{Z}_{>0},
\mathbb{Z}_{\geq 0} \mapsto \mathbb{Z}_{\geq 0},
\mathbb{Z} \mapsto \mathbb{Z}_{\geq 0}\}.\end{aligned}$$ Let us characterize the correctness kernel $\mathscr{K}_{{\ensuremath{\mathit{sq}}}}(\operatorname{Sign})$ by Theorem \[kernel\]. We have that $\operatorname{img}({\ensuremath{\mathit{sq}}}^{\operatorname{Sign}})= \{\varnothing, \mathbb{Z}_{>0}, 0, 
\mathbb{Z}_{\geq 0}\}$. Moreover, $$\begin{aligned}
\max (\{x\in \operatorname{Sign}~|~ {\ensuremath{\mathit{sq}}}^{\operatorname{Sign}}(x) = \varnothing\}) &= \{\varnothing\}\\
\max (\{x\in \operatorname{Sign}~|~ {\ensuremath{\mathit{sq}}}^{\operatorname{Sign}}(x) = \mathbb{Z}_{>0}\}) &= \{\mathbb{Z}_{\neq 0}\}\\ 
\max (\{x\in \operatorname{Sign}~|~ {\ensuremath{\mathit{sq}}}^{\operatorname{Sign}}(x) = 0\}) &= \{0\}\\
\max (\{x\in \operatorname{Sign}~|~ {\ensuremath{\mathit{sq}}}^{\operatorname{Sign}}(x) = \mathbb{Z}_{\geq 0}\}) &= \{\mathbb{Z}\}\end{aligned}$$ Therefore, $\bigcup_{y\in \operatorname{img}({\ensuremath{\mathit{sq}}}^{\operatorname{Sign}})} \max (\{x\in \operatorname{Sign}~|~ {\ensuremath{\mathit{sq}}}^{\operatorname{Sign}}(x) = y\}) 
= \{\varnothing,\mathbb{Z}_{\neq 0},0,\mathbb{Z}\}$ so that, by Theorem \[kernel\]: $$\mathscr{K}_{{\ensuremath{\mathit{sq}}}}(\operatorname{Sign}) = \operatorname{Cl}_{\cap}(\{\varnothing, \mathbb{Z}_{> 0}, 
0,\mathbb{Z}_{\geq 0}, \mathbb{Z}_{\neq 0}, \mathbb{Z}\}) = \operatorname{Sign}\smallsetminus
\{\mathbb{Z}_{< 0}, \mathbb{Z}_{\leq 0}\}.$$ Thus, it turns out that we can safely remove the abstract values $\mathbb{Z}_{< 0}$ and $\mathbb{Z}_{\leq 0}$ from $\operatorname{Sign}$ and still preserve the same b.c.a. as $\operatorname{Sign}$ does. Besides, we cannot remove further abstract elements otherwise we do not retain the same b.c.a. as $\operatorname{Sign}$. For example, this means that $\operatorname{Sign}$-based analyses of programs like $$x := k;
\textbf{while}~\text{condition}~ \textbf{do}
~x := x*x;$$ can be carried out by using the simpler domain $\operatorname{Sign}\smallsetminus
\{\mathbb{Z}_{< 0}, \mathbb{Z}_{\leq 0}\}$, yet providing the same input/output abstract behavior.

It is worth remarking that in Theorem \[kernel\] the hypothesis of continuity is crucial for the existence of correctness kernels and this is shown by the following example.

\[esempio1\] Let us consider as concrete domain $C$ the $\omega + 2$ ordinal, i.e., $C \triangleq \{ x\in \mathit{Ord}~|~ x
  < \omega\} \cup$, and let $f:C{\rightarrow}C$ be defined as follows: $$f(x) {\triangleq}\left\{
    \begin{array}{ll}
    \omega & \mbox{ if $x<\omega$;} \\
    \omega+1 &\mbox{ otherwise.}
    \end{array}
    \right.$$ Let $\mu\in \operatorname{uco}(C)$ be the identity $\lambda x.x$ uco, so that $\mu {\circ}f {\circ}\mu = f$. For any $k\geq 0$, consider $\rho_k\in \operatorname{uco}(C)$ defined as $\ok{\rho_k {\triangleq}C\smallsetminus [0,k[}$ and observe that for any $k$, we have that $\rho_k {\circ}f {\circ}\rho_k = f = \mu {\circ}f {\circ}\mu$. However, it turns out that $\sqcup_{k\geq 0} \rho_k = \cap_{k\geq 0} 
\operatorname{img}(\rho_k) =
\{\omega, \omega +1\}$. Hence, $(\sqcup_{k\geq 0} \rho_k) {\circ}f {\circ}(\sqcup_{k\geq 0} \rho_k) = \lambda x.\omega +1\neq \mu {\circ}f {\circ}\mu$. Hence, the correctness kernel of $\mu$ for $f$ does not exist. Observe that $\mu {\circ}f=f$ is clearly not continuous and therefore this example is consistent with Theorem \[kernel\].

Correctness Kernels in Abstract Model Checking
==============================================

Following the approach by Ranzato and Tapparo [@rt07], partitions of a state space $\Sigma$ can be viewed as particular abstract domains of the concrete domain $\wp(\Sigma)$. Let $\operatorname{Part}(\Sigma)$ denote the set of partitions of $\Sigma$. Given a partition $P\in \operatorname{Part}(\Sigma)$, the corresponding set of (possibly empty) unions of blocks of $P$, namely $\wp(P)$, is viewed as an abstract domain of $\wp(\Sigma)$ by means of the following Galois insertion $(\alpha_P, \wp(\Sigma)_\subseteq , \wp(P)_\subseteq, \gamma_P)$: $$\alpha_P(S) {\triangleq}\{B\in P~|~ B\cap S \neq \varnothing\}  
\text{~~and~~}
\gamma_P(\mathcal{B}) {\triangleq}\cup_{B\in \mathcal{B}} B.$$ Hence, the abstraction $\alpha_P(S)$ provides the minimal over-approximation of a set $S$ of states through blocks of $P$.

Consider a transition system $\mathcal{S} 
= \langle \Sigma, {\shortrightarrow}\rangle$ and a corresponding abstract transition system ${\mathcal{A}}=
\langle P, {\shortrightarrow}^\sharp \rangle$ defined over a state partition $P\in \operatorname{Part}(\Sigma)$.[^1] Fixpoint-based verification of a temporal specification on the abstract model ${\mathcal{A}}$ relies on the computation of least/greatest fixpoints of operators which are defined using Boolean connectives (union, intersection, complementation) on abstract states and abstract successor/predecessor functions $\operatorname{post}^\sharp$/$\operatorname{pre}^\sharp$ on the abstract transition system $\langle P,{\shortrightarrow}^\sharp\rangle$. The key point here is that successor/predecessor functions are defined as best correct approximations on the abstract domain $P$ of the corresponding concrete successor/predecessor functions. In standard abstract model checking [@bk08; @cgl94; @cgp99], the abstract transition relation is defined as the existential/existential relation ${\shortrightarrow}^{\exists\exists}$ between blocks of $P$, namely: $$\begin{gathered}
B {\shortrightarrow}^{\exists\exists} C \text{~~~~iff~~~~} \exists x\in B.\exists y\in C.\: x
{\shortrightarrow}y\\
\operatorname{post}^{\exists\exists}(B) {\triangleq}\{C\in P~|~B {\shortrightarrow}^{\exists\exists} C \};~~~~~~
\operatorname{pre}^{\exists\exists}(C) {\triangleq}\{B\in P~|~B {\shortrightarrow}^{\exists\exists} C\}.\end{gathered}$$ As shown in [@rt07], it turns out that $\operatorname{pre}^{\exists\exists}$ and $\operatorname{post}^{\exists\exists}$ are the best correct approximations of, respectively, $\operatorname{pre}$ and $\operatorname{post}$ functions on the above abstraction $(\alpha_P, \wp(\Sigma)_\subseteq , \wp(P)_\subseteq, \gamma_P)$. In fact, for a block $C\in P$, we have that $$\alpha_P(\operatorname{pre}(\gamma_P(C))) = \{B\in P~|~ B\cap \operatorname{pre}(C)\neq \varnothing\} 
= \operatorname{pre}^{\exists\exists}(C)$$ and an analogous equation holds for $\operatorname{post}$. We thus have that $\operatorname{pre}^{\exists\exists} = \alpha_P \circ \operatorname{pre}\circ \gamma_P$ and $\operatorname{post}^{\exists\exists} = \alpha_P \circ \operatorname{post}\circ \gamma_P$.

This abstract interpretation-based framework allows us to apply correctness kernels in the context of abstract model checking. The abstract transition system ${\mathcal{A}}= \langle P, {\shortrightarrow}^{\exists\exists} \rangle$ is viewed as an abstract interpretation defined by the abstract domain $(\alpha_P, \wp(\Sigma)_\subseteq ,$ $\wp(P)_\subseteq, \gamma_P)$ and the corresponding abstract functions $\operatorname{pre}^{\exists\exists} = \alpha_P \circ \operatorname{pre}\circ \gamma_P$ and $\operatorname{post}^{\exists\exists} = \alpha_P \circ \operatorname{post}\circ \gamma_P$. Then, the correctness kernel of the abstraction $\wp(P)$ for the concrete predecessor/successor $\{\operatorname{pre},\operatorname{post}\}$, that we denote simply by $\mathscr{K}_{{\shortrightarrow}}(P)$ (by Theorem \[kernel\], this clearly exists since $\operatorname{pre}$ and $\operatorname{post}$ are additive functions), provides a simplification of the abstract domain $\wp(P)$ that preserves the best correct approximations of predecessor and successor functions. This simplification $\mathscr{K}_{{\shortrightarrow}}(P)$ of the abstract state space $P$ works as follows:

\[kernel-part\] $\mathscr{K}_{{\shortrightarrow}}(P)$ merges two blocks $B_1,B_2\in P$ if and only if for any $A\in P$, $A {\shortrightarrow}^{\exists\exists} B_1 \:{\Leftrightarrow}\: A {\shortrightarrow}^{\exists\exists} B_2$ and $B_1 {\shortrightarrow}^{\exists\exists} A \:{\Leftrightarrow}\: B_2 {\shortrightarrow}^{\exists\exists} A$.

By Theorem \[kernel\], we have that the kernel $\mathscr{K}_{{\shortrightarrow}}(P)$ of the abstraction $\wp(P)\in \operatorname{Abs}(\wp(\Sigma))$ for $\operatorname{pre}$ and $\operatorname{post}$ is as follows: $$\begin{gathered}
\mathscr{K}_{{\shortrightarrow}}(P) = \operatorname{Cl}_{\cap} 
\Big(\operatorname{img}(\operatorname{pre}^{\exists\exists}) \cup \textstyle \bigcup_{\mathcal{C}\in \operatorname{img}(\operatorname{pre}^{\exists\exists})}
\cup \{\mathcal{B}\in \wp(P)~|~ \operatorname{pre}^{\exists\exists}(\mathcal{C}) = \mathcal{B}\}\\
\bigcup 
\operatorname{img}(\operatorname{post}^{\exists\exists}) \cup \textstyle \bigcup_{\mathcal{B}\in \operatorname{img}(\operatorname{post}^{\exists\exists})}
\cup \{\mathcal{C}\in \wp(P)~|~ \operatorname{post}^{\exists\exists}(\mathcal{B}) = \mathcal{C}\}
\Big).\end{gathered}$$ Let us observe that both b.c.a.’s $\operatorname{pre}_{\exists\exists}, \operatorname{post}_{\exists\exists}: \wp(P) {\rightarrow}\wp(P)$ are additive functions, so that for any $\mathcal{C}\in \operatorname{img}(\operatorname{pre}_{\exists\exists})$, $\cup \{\mathcal{B}\in \wp(P)~|~ \operatorname{pre}^{\exists\exists}(\mathcal{C}) = \mathcal{B}\} 
\in \operatorname{img}(\operatorname{pre}_{\exists\exists})$ and for any $\mathcal{B}\in \operatorname{img}(\operatorname{post}_{\exists\exists})$, $\cup \{\mathcal{C}\in \wp(P)~|~ \operatorname{post}^{\exists\exists}(\mathcal{B}) = \mathcal{C}\} 
\in \operatorname{img}(\operatorname{post}_{\exists\exists})$. Moreover, $\mathscr{K}_{{\shortrightarrow}}(P)$ is closed under arbitrary unions. Hence, the kernel can be simplified as follows: $$\mathscr{K}_{{\shortrightarrow}}(P) = \operatorname{Cl}_{\cap,\cup} (\{\operatorname{pre}^{\exists\exists} (\{C\})~|~
C\in P\} \cup \{\operatorname{post}^{\exists\exists} (\{B\})~|~
B\in P\}).$$ We therefore have that a block $B\in P$ is merged together with all the blocks $B'\in P$ such that for any block $A\in P$, $B \in \operatorname{pre}^{\exists\exists} (\{A\}) {\Leftrightarrow}B'  \in \operatorname{pre}^{\exists\exists} (\{A\})$ and $B \in \operatorname{post}^{\exists\exists} (\{A\}) {\Leftrightarrow}B'  \in \operatorname{post}^{\exists\exists} (\{A\})$. Thus, the thesis follows.

Reconsider the abstract transition system ${\mathcal{A}}$ in Section \[intro\] and let $P=\{[1],[2,3],[4,5],[6],[7],[8,9]\}$ be the underlying state partition. In this case, we have that $$\begin{array}{l}
\operatorname{img}(\operatorname{pre}^{\exists\exists}) = \operatorname{Cl}_{\cup} \big( \big\{ \{[1]\}, \{[2,3],[4,5]\}, \{[6],[7]\}\big\}\big),\\
\operatorname{img}(\operatorname{post}^{\exists\exists}) = \operatorname{Cl}_{\cup} \big(\big\{\{[2,3],[4,5]\}, \{[6],[7]\},\{[8,9]\}\big\}\big).
\end{array}$$ Hence, by Corollary \[kernel-part\], in the correctness kernel $\mathscr{K}_{{\shortrightarrow}}(P)$ the block $[2,3]$ is merged with $[4,5]$ while $[6]$ is merged with $[7]$. This therefore simplifies the partition $P$ to $P'' = \{[1], [2,3,4,5], [6,7], [8,9]\}$, that is, we obtain the abstract transition system ${\mathcal{A}}''$ in Section \[intro\].

Example Guided Abstraction Simplification {#egas}
=========================================

Let us discuss how correctness kernels give rise to an Example-Guided Abstraction Simplification (EGAS) paradigm in abstract transition systems.

Let us first recall some basic notions of CEGAR [@cgjlv00; @cgjlv03]. Consider an abstract transition system ${\mathcal{A}}=
\langle P, {\shortrightarrow}^{\exists\exists}\rangle$ defined over a state partition $P\in \operatorname{Part}(\Sigma)$ and a finite abstract path $\pi =
\langle B_1,...,B_n\rangle$ in ${\mathcal{A}}$, where each $B_i$ is a block of $P$. Typically, this is a path counterexample to the validity of a temporal formula that has been given as output by a model checker (for simplicity we do not consider here loop path counterexamples). The set of concrete paths that are abstracted to $\pi$ are defined as follows: $$\operatorname{paths}(\pi) {\triangleq}\{\tuple{s_1,...,s_n}\in \Sigma^n~|~\forall i\in [1,n]. s_i\in B_i \;\&\; \forall i\in [1,n). s_i {\shortrightarrow}s_{i+1}\}.$$ The abstract path $\pi$ is *spurious* when it represents no real concrete path, i.e., when $\operatorname{paths}(\pi)=\varnothing$. The sequence of sets of states $\operatorname{sp}(\pi) = 
\langle S_1,...,S_n\rangle$ is inductively defined as follows: $S_1 {\triangleq}B_1$; $S_{i+1} {\triangleq}\operatorname{post}(S_i)\cap B_{i+1}$. As shown in [@cgjlv03], it turns out that $\pi$ is spurious iff there exists a least $k\in [1,n-1]$ such that $S_{k+1}=\varnothing$. In such a case, the partition $P$ is refined by splitting the block $B_{k}$. The three following sets partition the states of the block $B_{k}$:

dead-end states: $B_{k}^{\text{dead}} {\triangleq}S_{k}\neq \varnothing$

bad states: $B_{k}^{\text{bad}} {\triangleq}B_{k} \cap \operatorname{pre}(B_{k+1}) \neq \varnothing$

irrelevant states: $B_{k}^{\text{irr}} {\triangleq}B_{k}\smallsetminus
(B_{k}^{\text{dead}} \cup B_{k}^{\text{bad}})$

The split of the block $B_{k}$ must separate dead-end states from bad states, while irrelevant states may be joined indifferently with dead-end or bad states. However, the problem of finding the coarsest refinement of $P$ that separates dead-end and bad states is NP-hard [@cgjlv03] and thus some refinement heuristics are used. According to the basic heuristics of CEGAR [@cgjlv03 Section 4], $B_{k}$ is simply split into $B_{k}^{\text{dead}}$ and $B_{k}^{\text{bad}} \cup B_{k}^{\text{irr}}$.

=\[-&gt;,&gt;=latex’\] (0,3) node\[name=1\][1]{} (0,1) node\[name=2\][2]{} (2,4) node\[name=3\][3]{} (2,2) node\[name=4\][4]{} (2,0) node\[name=5\][5]{} (4,3) node\[name=6\][6]{} (4,1) node\[name=7\][7]{}; (6,3.5) node\[name=f,rotate=45\][$\Longrightarrow$]{}; (6,0.5) node\[name=f,rotate=-45\][$\Longrightarrow$]{};

(0,4.5) node\[name=a\][$\mathcal{A}$]{}; (1) to (5); (2) to (4); (2) to (5); (3) to (6); (4) to (7); (5) to (7);

(1.north west) ++(-0.1,0.1) node\[name=a1\] (1.south east) ++(0.1,-0.1) node\[name=a2\]; (a1) rectangle (a2);

(2.north west) ++(-0.1,0.1) node\[name=a3\] (2.south east) ++(0.1,-0.1) node\[name=a4\]; (a3) rectangle (a4);

(3.north west) ++(-0.1,0.1) node\[name=b3\] (5.south east) ++(0.1,-0.1) node\[name=b4\]; (b3) rectangle (b4);

(6.north west) ++(-0.1,0.1) node\[name=c1\] (6.south east) ++(0.1,-0.1) node\[name=c2\]; (c1) rectangle (c2);

(7.north west) ++(-0.1,0.1) node\[name=c3\] (7.south east) ++(0.1,-0.1) node\[name=c4\]; (c3) rectangle (c4);

(8,6) node\[name=1\][1]{} (8,4) node\[name=2\][2]{} (10,7) node\[name=3\][3]{} (10,5) node\[name=4\][4]{} (10,3) node\[name=5\][5]{} (12,6) node\[name=6\][6]{} (12,4) node\[name=7\][7]{}; (14,3.5) node\[name=f,rotate=-45\][$\Longrightarrow$]{}; (8,7.5) node\[name=a\][$\mathcal{A}'$]{};

\(1) to (5); (2) to (4); (2) to (5); (3) to (6); (4) to (7); (5) to (7);

(1.north west) ++(-0.1,0.1) node\[name=a1\] (1.south east) ++(0.1,-0.1) node\[name=a2\]; (a1) rectangle (a2);

(2.north west) ++(-0.1,0.1) node\[name=a3\] (2.south east) ++(0.1,-0.1) node\[name=a4\]; (a3) rectangle (a4);

(3.north west) ++(-0.1,0.1) node\[name=b3\] (4.south east) ++(0.1,-0.1) node\[name=b4\]; (b3) rectangle (b4);

(5.north west) ++(-0.1,0.1) node\[name=b5\] (5.south east) ++(0.1,-0.1) node\[name=b6\]; (b5) rectangle (b6);

(6.north west) ++(-0.1,0.1) node\[name=c1\] (6.south east) ++(0.1,-0.1) node\[name=c2\]; (c1) rectangle (c2);

(7.north west) ++(-0.1,0.1) node\[name=c3\] (7.south east) ++(0.1,-0.1) node\[name=c4\]; (c3) rectangle (c4);

(8,0) node\[name=1\][1]{} (8,-2) node\[name=2\][2]{} (10,1) node\[name=3\][3]{} (10,-1) node\[name=4\][4]{} (10,-3) node\[name=5\][5]{} (12,0) node\[name=6\][6]{} (12,-2) node\[name=7\][7]{}; (8,1.5) node\[name=a\][$\mathcal{A}''$]{};

\(1) to (5); (2) to (4); (2) to (5); (3) to (6); (4) to (7); (5) to (7);

(1.north west) ++(-0.1,0.1) node\[name=a1\] (1.south east) ++(0.1,-0.1) node\[name=a2\]; (a1) rectangle (a2);

(2.north west) ++(-0.1,0.1) node\[name=a3\] (2.south east) ++(0.1,-0.1) node\[name=a4\]; (a3) rectangle (a4);

(3.north west) ++(-0.1,0.1) node\[name=b3\] (3.south east) ++(0.1,-0.1) node\[name=b4\]; (b3) rectangle (b4);

(4.north west) ++(-0.1,0.1) node\[name=b5\] (5.south east) ++(0.1,-0.1) node\[name=b6\]; (b5) rectangle (b6);

(6.north west) ++(-0.1,0.1) node\[name=c1\] (6.south east) ++(0.1,-0.1) node\[name=c2\]; (c1) rectangle (c2);

(7.north west) ++(-0.1,0.1) node\[name=c3\] (7.south east) ++(0.1,-0.1) node\[name=c4\]; (c3) rectangle (c4);

(16,3) node\[name=1\][1]{} (16,1) node\[name=2\][2]{} (18,4) node\[name=3\][3]{} (18,2) node\[name=4\][4]{} (18,0) node\[name=5\][5]{} (20,3) node\[name=6\][6]{} (20,1) node\[name=7\][7]{}; (16,4.5) node\[name=a\][$\mathcal{A}'''$]{};

\(1) to (5); (2) to (4); (2) to (5); (3) to (6); (4) to (7); (5) to (7);

(1.north west) ++(-0.1,0.1) node\[name=a1\] (1.south east) ++(0.1,-0.1) node\[name=a2\]; (a1) rectangle (a2);

(2.north west) ++(-0.1,0.1) node\[name=a3\] (2.south east) ++(0.1,-0.1) node\[name=a4\]; (a3) rectangle (a4);

(3.north west) ++(-0.1,0.1) node\[name=b3\] (3.south east) ++(0.1,-0.1) node\[name=b4\]; (b3) rectangle (b4);

(4.north west) ++(-0.1,0.1) node\[name=b7\] (4.south east) ++(0.1,-0.1) node\[name=b8\]; (b7) rectangle (b8);

(5.north west) ++(-0.1,0.1) node\[name=b5\] (5.south east) ++(0.1,-0.1) node\[name=b6\]; (b5) rectangle (b6);

(6.north west) ++(-0.1,0.1) node\[name=c1\] (6.south east) ++(0.1,-0.1) node\[name=c2\]; (c1) rectangle (c2);

(7.north west) ++(-0.1,0.1) node\[name=c3\] (7.south east) ++(0.1,-0.1) node\[name=c4\]; (c3) rectangle (c4);

Let us see a simple example. Consider the abstract path $\pi=\langle[1], [345], [6]\rangle$ in the abstract transition system ${\mathcal{A}}$ depicted in Figure \[figura-bis\]. This is a spurious path and the block $[345]$ is therefore partitioned as follows: $[5]$ dead-end states, $[3]$ bad states and $[4]$ irrelevant states. The refinement heuristics of CEGAR tells us that irrelevant states are joined with bad states so that ${\mathcal{A}}$ is refined to the abstract transition system ${\mathcal{A}}'$. In turn, consider the spurious path $\pi' = \langle [2], [34], [6] \rangle$ in ${\mathcal{A}}'$, so that CEGAR refines ${\mathcal{A}}'$ to ${\mathcal{A}}'''$ by splitting the block $[34]$. In the first abstraction refinement, let us observe that if irrelevant states would have been joined together with dead-end states rather than with bad states we would have obtained the abstract system ${\mathcal{A}}''$, and ${\mathcal{A}}''$ does not contain spurious paths so that it surely does not need to be further refined.

EGAS can be integrated within the CEGAR loop thanks to the following remark. If $\pi_1$ and $\pi_2$ are paths, respectively, in $\tuple{P_1,{\shortrightarrow}^{\exists\exists}}$ and $\tuple{P_2,{\shortrightarrow}^{\exists\exists}}$, where $P_1,P_2\in \operatorname{Part}(\Sigma)$ and $P_1$ is finer than $P_2$, i.e.  $P_1\preceq P_2$, then we say that $\pi_1$ is abstracted to $\pi_2$, denoted by $\pi_1 \sqsubseteq \pi_2$, when $\operatorname{length}(\pi_1)=\operatorname{length}(\pi_2)$ and for any $j\in [1,\operatorname{length}(\pi_1)]$, $\pi_1(j)\subseteq \pi_2(j)$.

\[coro2\] Consider an abstract transition system ${\mathcal{A}}=\tuple{P,{\shortrightarrow}^{\exists\exists}}$ over a partition $P\in \operatorname{Part}(\Sigma)$ and its simplification ${\mathcal{A}}_s=\tuple{\mathscr{K}_{{\shortrightarrow}}(P),{\shortrightarrow}^{\exists\exists}}$ induced by the correctness kernel $\mathscr{K}_{{\shortrightarrow}}(P)$. If $\pi$ is a spurious abstract path in ${\mathcal{A}}_s$ then there exists a spurious abstract path $\pi'$ in ${\mathcal{A}}$ such that $\pi'\sqsubseteq \pi$.

This is a simple consequence of Corollary \[kernel-part\]. Let $\pi = \langle B_1,...,B_n\rangle$, where $B_i \in \mathscr{K}_{{\shortrightarrow}}(P)$, and let $B_k$ be the block of $\pi$ that causes the spuriousness of $\pi$. Then, for each $i\in [1,n]$, we have that $B_i = \cup C_i^{j_i}$, where $C_i^{j_i} \in P$. By Corollary \[kernel-part\], for each $i\in [1,n[$ and $j_i$, $\operatorname{post}^{\exists\exists} 
(B_i) = \operatorname{post}^{\exists\exists} (C_i^{j_i})$ and for each $i\in ]1,n]$ and $j_i$, $\operatorname{pre}^{\exists\exists} 
(B_i) = \operatorname{pre}^{\exists\exists} (C_i^{j_i})$. Then, in order to define the path $\pi'$ in ${\mathcal{A}}$, for $i \in [1,n]$, one can choose any block $C_i^{j_i}$ in $P$ such that $C_i^{j_i} \subseteq B_i$. The key point to note here is that the definition of the correctness kernel $\mathscr{K}_{{\shortrightarrow}}(P)$ guarantees that $C_k^{j_k}$ causes the spuriousness of $\pi'$ and that $\pi' \sqsubseteq \pi$.

Thus, it turns out that the abstraction simplification induced by the correctness kernel does not add spurious paths. These observations suggest us a new refinement strategy within the CEGAR loop. Let $\pi = \langle B_1,...,B_n\rangle$ be a spurious path in ${\mathcal{A}}$ and $\operatorname{sp}(\pi) = 
\langle S_1,...,S_n\rangle$ such that $S_{k+1}=\varnothing$ for some minimum $k\in [1,n-1]$, so that the block $B_{k}$ needs to be split. The set of irrelevant states $B_{k}^{\text{irr}}$ is partitioned as follows. We first define the subset of *bad-irrelevant* states $B_{k}^{\text{bad-irr}}$. Let $\operatorname{pre}^{\exists\exists}(B_{k}^{\text{bad}}) = \{A_1,...,A_j\}$ and $\operatorname{post}^{\exists\exists}(B_{k}^{\text{bad}})= \{C_1,...,C_l\}$. Then, we define: $$B_{k}^{\text{bad-irr}} {\triangleq}\big(\operatorname{post}(A_1 \cup ...\cup A_j) \cap 
\operatorname{pre}(C_1 \cup ... \cup C_l)\big) \cap B_{k}^{\text{irr}}.$$ The underlying idea is simple: $B_{k}^{\text{bad-irr}}$ contains the irrelevant states that: (1) can be reached from a block that reaches some bad state and (2) reach a block that is also reached by some bad state. By Corollary \[coro2\], it is therefore clear that by merging $B_{k}^{\text{bad-irr}}$ and $B_{k}^{\text{bad}}$ no spurious path is added w.r.t. the abstract system where they are kept separate. The subset of *dead-irrelevant* states $B_{k}^{\text{dead-irr}}$ is analogosly defined: If $\operatorname{pre}^{\exists\exists}(B_{k}^{\text{dead}}) = \{A_1,...,A_j\}$ and $\operatorname{post}^{\exists\exists}(B_{k}^{\text{dead}})= \{C_1,...,C_l\}$ then $$B_{k}^{\text{dead-irr}} {\triangleq}\big(\operatorname{post}(A_1 \cup ...\cup A_j) \cap 
\operatorname{pre}(C_1 \cup ... \cup C_l)\big) \cap B_{k}^{\text{irr}}.$$ It may happen that: (A) an irrelevant state is both bad- and dead-irrelevant; (B) an irrelevant state is neither bad- nor dead-irrelevant. From the viewpoint of EGAS, the states of case (A) can be equivalently merged with bad or dead states since in both cases no spurious path is added. On the other hand, the states of case (B) are called *fully-irrelevant* because EGAS does not provide a merging strategy with bad or dead states. For these states, one could use, for example, the basic refinement heuristics of CEGAR that merge them with bad states.

In the above example, for the spurious path $\tuple{[1],[3,4,5],[6]}$ in ${\mathcal{A}}$, the block $B=[3,4,5]$ needs to be refined: $$B^{\text{bad}}=[3],\; B^{\text{dead}}=[5],\; 
B^{\text{irr}}=[4].$$ Here, $4$ is a dead-irrelevant state because $\operatorname{pre}^{\exists\exists}([5]) = \{[1],[2]\}$, $\operatorname{post}^{\exists\exists}([5])= \{[7]\}$ and $(\operatorname{post}([1]\cup [2]) \cap 
\operatorname{pre}([7])) \cap [4] = \{4\}$. Hence, according to the EGAS refinement strategy, the dead-irrelevant state $4$ is merged in ${\mathcal{A}}''$ with the dead-end state $5$.

Correctness Kernels in Predicate Abstraction
============================================

Let us discuss how correctness kernels can be also used in the context of predicate abstraction-based model checking [@ddp99; @gs97]. Following Ball et al.’s approach [@bpr03], predicate abstraction can be formalized by abstract interpretation as follows. Let us consider a program $P$ with $k$ integer variables $x_1$,...,$x_k$. The concrete domain of computation of $P$ is $\tuple{\wp(\operatorname{States}),\subseteq}$ where $\operatorname{States}{\triangleq}\{x_1,...,x_k\} \rightarrow \mathbb{Z}$. Values in $\operatorname{States}$ are denoted by tuples $\tuple{z_1,...,z_k}\in \mathbb{Z}^k$. The program $P$ generates a transition system $\tuple{\operatorname{States},{\shortrightarrow}}$ so that the concrete semantics of $P$ is defined by the corresponding successor function $\operatorname{post}:\wp(\operatorname{States}) {\rightarrow}\wp(\operatorname{States})$.

A finite set $\mathcal{P} = \{p_1,...,p_n\}$ of state predicates is considered, where each predicate $p_i$ denotes the subset of states that satisfy $p_i$, i.e. $\{s\in \operatorname{States}~|~ s \models p_i\}$. These predicates give rise to the so-called *Boolean abstraction* $B {\triangleq}\langle \wp(\{0,1\}^n),\subseteq \rangle$ which is related to $\wp(\operatorname{States})$ through the following abstraction and concretization maps (here, $s\models p_i$ is understood in $\{0,1\}$):

$$\begin{aligned}
\alpha_B(S) &{\triangleq}\{\langle s\models p_1,...,s\models p_n \rangle \in 
\{0,1\}^n ~|~ s\in S\},\\
\gamma_B(V) &{\triangleq}\{s\in \operatorname{States}~|~ \langle s\models p_1,...,s\models p_n \rangle 
\in V\}.\end{aligned}$$

These functions give rise to a disjunctive (i.e., $\gamma$ preserves lub’s) Galois connection $(\alpha_B, 
\wp(\operatorname{States})_\subseteq, \wp(\{0,1\}^n)_\subseteq, \gamma_B)$.

Verification of reachability properties based on predicate abstraction consists in computing the least fixpoint of the best correct approximation of $\operatorname{post}$ on the Boolean abstraction $B$, namely, $\operatorname{post}^B {\triangleq}\alpha_B {\circ}\operatorname{post}{\circ}\gamma_B$. As argued in [@bpr03], the Boolean abstraction $B$ may be too costly for the purpose of reachability verification, so that one usually abstracts $B$ through the so-called *Cartesian abstraction*. This latter abstraction formalizes precisely the abstract $\operatorname{post}$ operator computed by the verification algorithm of the c2bp tool in SLAM [@slam02]. However, the Cartesian abstraction of $B$ may cause a loss of precision, so that this abstraction is successively refined by reduced disjunctive completion and the so-called focus operation, and this formalizes the bebop tool in SLAM [@bpr03].

$x$, $y$, $z$, $w$;

$\mathit{foo}$() {

     {

        $z := 0$;  $x:=y$;

         $(w)$ { $x$++; $z:=1$; }

    } $(!(x = y))$

     $(z)$

        $(0)$;    $(*)$

}

Let us consider the example program in Figure \[exprog\], taken from [@bpr03], where the goal is that of verifying that the assert at line $(*)$ is never reached, regardless of the context in which $\mathit{foo}()$ is called. Ball et al. [@bpr03] consider the following set of predicates $\mathcal{P} {\triangleq}\{p_1 \equiv (z = 0), p_2 \equiv (x=y)\}$ so that the Boolean abstraction is $B = \wp(\{\tuple{0,0},\tuple{0,1},\tuple{1,0},\tuple{1,1}\})_\subseteq$. Clearly, the analysis based on $B$ allows to conclude that line $(*)$ is not reachable. This comes as a consequence of the fact that the least fixpoint computation of the best correct approximation $\operatorname{post}^B$ for the do-while loop provides as result $\{ \tuple{0,0}, \tuple{1,1}\}\in B$ because: $$\begin{aligned}
\varnothing \xrightarrow{z:=0;~ x:=y}\{\tuple{1,1}\}  
\xrightarrow{\textbf{if}(w) \{x\text{++};~z:=1;\}}
\{\tuple{1,1}\} \cup \{\tuple{0,0}\} \end{aligned}$$ where, according to a standard approach, the guard of the if statement is simply ignored. Hence, at the exit of the do-while loop one can conclude that $$\begin{aligned}
\{\tuple{1,1},\tuple{0,0}\}\cap p_2 = \{\tuple{1,1},\tuple{0,0}\}\cap 
\{\tuple{0,1},\tuple{1,1}\} = \{\tuple{1,1}\}\end{aligned}$$ holds, hence $p_1$ is satisfied, so that $z=0$ and therefore line $(*)$ can never be reached.

Let us characterize the correctness kernel of the Boolean abstraction $B$. Let $S_1 {\triangleq}z:=0;~ x:=y$ and $S_2 {\triangleq}x\text{++};~z:=1$. The best correct approximations of $\operatorname{post}_{S_1}$ and $\operatorname{post}_{S_2}$ on the abstract domain $B$ turn out to be as follows: $$\begin{aligned}
\alpha_B {\circ}\operatorname{post}_{S_1} {\circ}\gamma_B = \Big\{&
\tuple{0,0} \mapsto \{\tuple{1,1}\}, \tuple{0,1} \mapsto \{\tuple{1,1}\}, 
\tuple{1,0} \mapsto \{\tuple{1,1}\},\\[-5pt]
& \tuple{1,1} \mapsto \{\tuple{1,1}\} \Big\}\\
\alpha_B {\circ}\operatorname{post}_{S_2} {\circ}\gamma_B = \Big\{ &
\tuple{0,0} \mapsto \{\tuple{0,0},\tuple{0,1}\}, \tuple{0,1} \mapsto \{\tuple{0,0}\}, \\[-5pt]
& \tuple{1,0} \mapsto \{\tuple{0,0},\tuple{0,1}\}, 
\tuple{1,1} \mapsto \{\tuple{0,0}\} \Big\}\end{aligned}$$ Thus, we have that $\operatorname{img}(\alpha_B {\circ}\operatorname{post}_{S_1} {\circ}\gamma_B) = \{\{\tuple{1,1}\}\}$ and $\operatorname{img}(\alpha_B {\circ}\operatorname{post}_{S_2} {\circ}\gamma_B) = \{\{\tuple{0,0},\tuple{0,1}\}, 
\{\tuple{0,0}\} \}$ so that $$\begin{aligned}
\max\big(\{V\in B~|~ \alpha_B(\operatorname{post}_{S_1}(\gamma_B(V))) = \{\tuple{1,1}\}\}\big) &= 
\{\{\tuple{0,0}, \tuple{0,1}, \tuple{1,0}, \tuple{1,1}\}\}\\
\max\big(\{V\in B~|~ \alpha_B(\operatorname{post}_{S_2}(\gamma_B(V))) = \{\tuple{0,0},\tuple{0,1}\}\}\big) 
&=  \{\{\tuple{0,0}, \tuple{0,1}, \tuple{1,0}, \tuple{1,1}\}\}\\
\max\big(\{V\in B~|~ \alpha_B(\operatorname{post}_{S_2}(\gamma_B(V))) = \{\tuple{0,0}\}\}\big) 
 &=  \{\{\tuple{0,1}, \tuple{1,1}\}\}\end{aligned}$$

Hence, by Theorem \[kernel\], the kernel $\mathscr{K}_F(B)$ of $B$ for $F{\triangleq}\{\operatorname{post}_{S_1}, 
\operatorname{post}_{S_2}\}$ is: $$\begin{aligned}
\operatorname{Cl}_\cap \Big( \operatorname{Cl}_\cup \big( 
\big\{ &
\{\tuple{0,0}\},
\{\tuple{1,1}\}, 
\{\tuple{0,0},\tuple{0,1}\}, \{\tuple{0,1},\tuple{1,1}\},
\\[-5pt]
&
\{\tuple{0,0},\tuple{0,1},\tuple{1,0},\tuple{1,1}\}
\big\}  
\big) \Big) = \operatorname{Cl}_\cup \Big( \big\{  
\{\tuple{0,0}\},
\{ \tuple{0,1}\},
\{ \tuple{1,1}\}
\big\} \Big) \end{aligned}$$ where we observe that the set $\{\tuple{0,1}\}$ is obtained as the intersection $\{\tuple{0,0},\tuple{0,1}\} \cap \{\tuple{0,1},\tuple{1,1}\}$. This correctness kernel $\mathscr{K}_F(B)$ can be therefore represented as $$\tuple{\wp(\{\tuple{0,0},\tuple{0,1},\tuple{1,1}\}) \cup \{\tuple{0,0},
\tuple{0,1}, \tuple{1,0}, \tuple{1,1}\},\subseteq}.$$ Thus, it turns out that $\mathscr{K}_F(B)$ is a proper abstraction of the Boolean abstraction $B$ that, for example, is not able to express precisely the property $p_1 \wedge \neg p_2 \equiv (z=0) \wedge (x\neq y)$.

It is interesting to compare this correctness kernel $\mathscr{K}_F(B)$ with Ball et al.’s [@bpr03] Cartesian abstraction of $B$. The Cartesian abstraction is defined as $$C{\triangleq}\tuple{\{0,1,*\}^n \cup \{\bot_C\},\leq}$$ where $\leq$ is the componentwise ordering between tuples of values in $\{0,1,*\}$ ordered by $0 < *$ and $1< *$ ($\bot_C$ is a bottom element that represents the empty set of states). The concretization function $\gamma_{C} :
C\rightarrow \wp(\operatorname{States})$ is as follows: $$\gamma_{C} (\tuple{v_1,...,v_n}) {\triangleq}\{s\in \operatorname{States}~|~
\tuple{s\models p_1,...,s\models p_n} \leq \tuple{v_1,...,v_n}\}.$$ It turns out that these two abstractions are not comparable. For instance, $\tuple{1,0}\in C$ represents $p_1 \wedge \neg p_2$ which is instead not represented by $\mathscr{K}_F(B)$, while $\{\tuple{0,0},\tuple{1,1}\}\in \mathscr{K}_F(B)$ represents $(\neg p_1 \wedge \neg p_2) \vee (p_1 \wedge p_2)$ which is not represented in $C$. However, while the correctness kernel guarantees no loss of information in analyzing the program $P$ (and therefore the analysis with $\mathscr{K}_F(B)$ concludes that $(*)$ cannot be reached), the analysis of $P$ with the Cartesian abstraction $C$ is inconclusive because: $$\begin{aligned}
\bot_C \xrightarrow{z:=0;~ x:=y} \tuple{1,1}  
\xrightarrow{\textbf{if}(w) \{x\text{++};~z:=1;\}}
\tuple{0,0} \vee_C \tuple{1,1} = \tuple{*,*} \end{aligned}$$ where $\gamma_C(\tuple{*,*}) = 
\operatorname{States}$, so that at the exit of the do-while loop one cannot infer with $C$ that line $(*)$ is unreachable.

Related and Future Work
=======================

Few examples of abstraction simplifications are known. A general notion of domain simplification and compression in abstract interpretation has been introduced in [@fgr96; @gr97] as a formal dual of abstraction refinement. This duality has been further exploited in [@gm08] to include semantics transformations in a general theory for transforming abstractions and semantics based on abstract interpretation. Our domain transformation does not fit directly in this framework. Following [@gr97], given a property $\mathcal{P}$ of abstract domains, the so-called core of an abstract domain $A$, when it exists, provides the most concrete simplification of $A$ that satisfies the property $\mathcal{P}$, while the so-called compressor of $A$, when it exists, provides the most abstract simplification of $A$ that induces the same refined abstraction in $\mathcal{P}$ as $A$ does. Examples of compressors include the least disjuctive basis [@gr98], where $\mathcal{P}$ is the abstract domain property of being disjunctive, and examples of cores include the completeness core [@grs00], where $\mathcal{P}$ is the domain property of being complete for some semantic function. The correctness kernel defined in this paper is neither an instance of a domain core nor an instance of a domain compression. The first because, given an abstraction $A$, the correctness kernel of $A$ characterizes the most abstract domain that induces the same best correct approximation of a function $f$ on $A$, whilst the notion of domain core for the domain property $\mathcal{P}_A$ of inducing the same b.c.a. as $A$ would not be meaningful, as this would trivially yield $A$ itself. The second because there is no (unique) maximal domain refinement of an abstract domain which induces the same property $\mathcal{P}_A$.

The EGAS methodology opens some stimulating directions for future work, such as (1) the formalization of a precise relationship between EGAS and CEGAR and (2) an experimental evaluation of the integration in the CEGAR loop of the EGAS-based refinement strategy of Section \[egas\]. It is here useful to recall that some work formalizing CEGAR in abstract interpretation has already been done [@CGR07; @gq01]. On the one hand, [@gq01] shows that CEGAR corresponds to iteratively compute a so-called complete shell [@grs00] of the underlying abstract model $A$ with respect to the concrete successor transformer, while [@CGR07] formally compares CEGAR with an abstraction refinement strategy based on the computations of abstract fixpoints in an abstract domain. These works can therefore provide a starting point for studying the relationship between EGAS and CEGAR in a common abstract interpretation setting.

#### **Acknowledgements.**

This work was carried out during a visit of the authors to the Equipe “Abstraction” lead by P. and R. Cousot, at École Normale Supérieure, Paris. This work was partially supported by the University of Padova under the Projects AVIAMO and BECOM.

[99]{}

C. Baier and J.-P. Katoen. *Principles of Model Checking*. The [M]{}[I]{}[T]{} Press, 2008.

T. Ball, A. Podelski and S.K. Rajamani. Boolean and [C]{}artesian abstraction for model checking [C]{} programs. *Int. J. Softw. Tools Technol. Transfer*, 5:49-58, 2003.

T. Ball and S.K. Rajamani. The SLAM Project: Debugging system software via static analysis. In *Proc. 29th ACM POPL*, pp. 1-3, 2002.

E.M. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith. Counterexample-guided abstraction refinement. In *Proc. 12th CAV*, LNCS 1855, pp. 154-169, 2000

E.M. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. *J. ACM*, 50(5):752-794, 2003.

E.M. Clarke, O. Grumberg and D. Long. Model checking and abstraction. *ACM Trans. Program. Lang. Syst.*, 16(5):1512–1542, 1994.

E.M. Clarke, O. Grumberg and D.A. Peled. *Model checking*. The [M]{}[I]{}[T]{} Press, 1999.

P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In *Proc. 4th ACM POPL*, pp. 238–252, 1977.

P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In *Proc. 6th ACM POPL*, pp. 269–282, 1979.

P. Cousot, P. Ganty and J.-F. Raskin Fixpoint-guided abstraction refinements. In *Proc. 14th SAS*, LNCS 4634, pp. 333-348, 2007.

S. Das, D.L. Dill, S. Park. Experience with predicate abstraction. In *Proc. 11th CAV*, LNCS 1633, pp. 160-171, 1999.

G. Filé, R. Giacobazzi, and F. Ranzato. A unifying view of abstract domain design. , 28(2):333-336, 1996.

R. Giacobazzi and I. Mastroeni. Transforming abstract interpretations by abstract interpretation (Invited Lecture). In [*Proc. 15th SAS*]{}, LNCS 5079, pp. 1-17, 2008.

R. Giacobazzi and E. Quintarelli. Incompleteness, counterexamples, and refinements in abstract model checking. In *Proc. 8th SAS*, LNCS 2126, pp. 356-373, 2001.

R. Giacobazzi and F. Ranzato. Refining and compressing abstract domains. In *Proc. 24th ICALP*, LNCS 1256, pp. 771-781, 1997.

R. Giacobazzi and F. Ranzato. Optimal domains for disjunctive abstract interpretation. *Sci. Comp. Program.*, 32:177–210, 1998.

R. Giacobazzi and F. Ranzato. Example-guided abstraction simplification. In *Proc. 37th ICALP*, LNCS 6199, pp. 211-222, 2010.

R. Giacobazzi, F. Ranzato and F. Scozzari. Making abstract interpretations complete. *J. ACM*, 47(2):361-416, 2000.

S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In *Proc. 9th CAV*, LNCS 1254, pp. 72-83, 1997.

F. Ranzato and F. Tapparo. Generalized strong preservation by abstract interpretation. *J. Logic and Computation*, 17(1):157-197, 2007.

[^1]: Equivalently, the abstract transition system ${\mathcal{A}}$ can be defined over an abstract state space $A$ determined by a surjective abstraction function $h:\Sigma {\rightarrow}A$.
