## 4 Preliminaries: Abstract Interpretation  
Abstract Interpretation [13] is a mathematical framework, originally introduced by [PERSON] and [PERSON] in 1977, which provides a sound approximation of programs concrete semantics enabling sound answers to questions about programs run-time behaviors. The framework has been applied to different applications areas, from Security (e.g., [30; 31]) to Databases (e.g., [32; 33]), and to different programming environments (e.g., [34; 35; 36]). The idea is to lift concrete semantics to an abstract setting by replacing concrete values by suitable properties of interest, and simulating the concrete operations by sound abstract operations. The concrete and the abstract domains are always partial orders, where the ordering relation describes the relative precision of the denotations and where the top element represents no information. The mapping between concrete and abstract semantics domains is established by Galois connection:  
**Definition 1** (Galois connections [13]).: _Consider two partial orders (\(\mathbb{D}\), \(\leqslant\)) and (\(\overline{\mathbb{D}}\), \(\sqsubseteq\)) where the first one represents a concrete domain and the second one represents an abstract domain.The Galois connection between \(\mathbb{D}\) and \(\overline{\mathbb{D}}\) is denoted by \(\left\langle(\mathbb{D},\leqslant)\), \(\alpha\), \(\gamma\), \((\overline{\mathbb{D}},\sqsubseteq)\right\rangle\) or \((\mathbb{D},\leqslant)\xleftarrow{\alpha\over\gamma}\)\((\overline{\mathbb{D}},\sqsubseteq)\) where \(\alpha\): \(\mathbb{D}\rightarrow\overline{\mathbb{D}}\) and \(\gamma\): \(\overline{\mathbb{D}}\rightarrow\mathbb{D}\) holds iff:_  
* \(\forall\upsilon\in\mathbb{D}\)_._ \(\upsilon\sqsubseteq\gamma\circ\alpha(\upsilon)\)_._
* \(\forall\overline{\upsilon}\in\overline{\mathbb{D}}\)_._ \(\alpha\circ\gamma(\overline{\upsilon})\sqsubseteq\overline{\upsilon}\)_._
* \(\alpha\) _and_ \(\gamma\) _are monotonic.__In other words, iff \(\forall v\in\mathbb{D},\overline{v}\in\overline{\mathbb{D}}\). \(\alpha(v)\sqsubseteq\overline{v}\iff v\leqslant\gamma(\overline{v})\)._  
For example, given a domain of integers \(Z\), we can establish a Galois connection \(\left\langle(\wp(Z),\subseteq),\right.\)\(\left.\alpha,\gamma,(\text{SIGN},\sqsubseteq)\right\rangle\) between the concrete domain \(\wp(Z)\), the powerset of \(Z\), and an abstract domain SIGN=\(\{\tau,+,-,0,\pm,0+,0-,\perp\}\) representing sign properties of numerical values, depicted in Figure 3.  
The abstraction function \(\alpha\) and concretization function \(\gamma\) between the domains are defined below:  
\[\forall X\in\wp(Z):\:\alpha(S) =\left\{\begin{array}{ll}\perp&\text{if }S=\emptyset\\ +&\text{if }S=\{\,a\,|\,a>0\,\}\\ 0&\text{if }S=\{\,0\,\}\\ -&\text{if }S=\{\,a\,|\,a<0\,\}\\ \pm&\text{if }S=\{\,a\,|\,a>0\,\,\forall\,a<0\,\}\\ 0+&\text{if }S=\{\,a\,|\,a\geqslant 0\,\}\\ 0-&\text{if }S=\{\,a\,|\,a\leqslant 0\,\}\\ \tau&\text{Otherwise}\end{array}\right.\] \[\forall\overline{v}\in\text{SIGN:}\gamma(\overline{v}) =\left\{\begin{array}{ll}\emptyset&\text{if }\overline{v}=\perp\\ \{k\in Z\,|\,\,k>0\}&\text{if }\overline{v}=+\\ \{0\}&\text{if }\overline{v}=0\\ \{k\in Z\,|\,\,k<0\}&\text{if }\overline{v}=-\\ \{k\in Z\,|\,\,k>0\lor k<0\}&\text{if }\overline{v}=\pm\\ \{k\in Z\,|\,\,k\geqslant 0\}&\text{if }\overline{v}=0+\\ \{k\in Z\,|\,\,k\leqslant 0\}&\text{if }\overline{v}=0-\\ Z&\text{Otherwise}\end{array}\right.\]  
The arithmetic operations over the abstract domain are defined accordingly, ensuring the soundness w.r.t. their concrete counter-part [37]. For example, the '\(\times\)' operation over the concrete domain is mapped to its abstract version '\(\times\)' as follows: \(-(\times^{\sharp})-=+,+(\times^{\sharp})-=-,+(\times^{\sharp})+=+,\tau( \times^{\sharp})+=\tau\), \(\perp(\times^{\sharp})+=\perp\), and so on.  
A number of abstract domains, non-relational and relational, exist in the literature [13; 37; 38; 39; 40].