# Hardware Model Checking Algorithms and Techniques
## 5 Interpolation-Based Model Checking
### [PERSON]'s Interpolation Algorithm  
[PERSON] [44] introduced the first complete algorithm for symbolic model checking based on [PERSON]'s interpolation. In the literature, such an algorithm is called _standard interpolation_ or just ITP for short. The algorithm computes [PERSON]'s interpolants to overapproximate reachable states of the system. The interpolants, as mentioned in the previous section, are computed from refutation proofs of unsatisfiable BMC runs. The algorithm comprises two nested loops. The outer loop is presented in procedure \(\textsc{ItpModelChecking}(\text{Algorithm \ref{alg:LPC}})\) whereas the inner loop is presented in procedure \(\textsc{ApproxForwardTraversal}(\text{Algorithm \ref{alg:LPC}})\). At each outer loop iteration, \(\textsc{ApproxForwardTraversal}\) is invoked to perform an overapproximated forward traversal of the reachable states while preserving safety with respect to a backward unrolling from the target (_bad cone_). \(\textsc{ApproxForwardTraversal}\) can be seen as computing a safe monotonic trace. Note that such a trace is not explicitly maintained. Only its final frame is kept at each iteration and used as base for computing the next one. We describe Algorithm 5 first. The procedure ApproxForwardTraversal operates a forward traversal in which interpolation is used as an overapproximated image operator. At each iteration, the procedure checks a BMC formula of fixed length \(k\), composed of two parts:  
* \(A\stackrel{{\text{def}}}{{=}}R(V^{0})\wedge T(V^{0},V^{1})\)
* \(B\stackrel{{\text{def}}}{{=}}Cone(1,k)=\Pi(1,k)\wedge\psi_{i=1}^{k }\
eg P(V^{i})\)  
where \(R\) is a set of overapproximated forward reachable states. In such a scenario, \(A\) represents the image of the set of states at the current traversal step, whereas \(B\) represents the set of backward reachable bad states, reachable in at most \(k-1\) transitions from the target. ```
0:\(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) a transition system; \(P\) a property over \(V\). 0:\(\langle\textit{res},\textit{cex}\rangle\) with \(\textit{res}\in\{\text{\sc Success},\text{\sc Fail}\}\); \(\textit{cex}\) a (possibly empty) initial path representing a counterexample. 1:procedureItpModelChecking(\(\mathcal{M}\), \(P\))
2:if\(\exists s_{0}\models\mathcal{I}(V)\wedge\
eg P(V)\)then
3:return\(\langle\textsc{Fail},\langle s_{0}\rangle\rangle\)
4:\(k\gets 1\)
5:whiletruedo
6:\(\langle\textit{res},\textit{cex}\rangle\leftarrow\textsc{ApproxForwardTraversal}( \mathcal{M},P,k)\)
7:ifres is Unreachthen
8:return\(\langle\textsc{Success},-\rangle\)
9:elseifres is Reachthen
10:return\(\langle\textsc{Fail},\textit{cex}\rangle\)
11:\(k\gets k+1\)
```  
**Algorithm 4** Top-level procedure of [PERSON]'s interpolation algorithm. This iterates overapproximated forward traversals of reachable states while keeping safety with respect to a bad cone of increasing depth from the target. At the first iteration, \(R\) is the set of initial states \(\mathcal{I}\) (line 2) and therefore is not overapproximated. In that case, the formula \(A\wedge B\) is exactly a BMC formula of length \(k\). If such a formula is satisfiable, the algorithm has found a counterexample \(\pi^{0,k}\) of length at most \(k\) (lines 3-4). Then, both the nested and the top-level procedures terminate, returningthe counterexample found. Otherwise, the algorithm starts traversing the reachable state space, computing overapproximated images by means of interpolation (lines 5-14). After composing \(A\) and \(B\) (lines 6-7), the algorithm checks whether \(A\wedge B\) is satisfiable (line 8). If that is the case, a (possibly spurious) counterexample \(\pi^{0,k}\) is found, i.e., a path of length at most \(k\) from the overapproximated set \(R\) to a bad state in \(Cone(1,k)\). Since \(R\) is an overapproximation of the reachable states, the algorithm cannot determine whether \(\pi^{0,k}\) is a _real counterexample_ or a _spurious counterexample_. Therefore, the procedure aborts the current forward traversal and returns the control to the top-level procedure.