# Hardware Model Checking Algorithms and Techniques
## 7 Igr
### Incremental State Sets in Interpolation  
In order to enable the reuse of previously computed interpolants, in IGR, a trace of overapproximations to reachable states is maintained and incrementally refined. Since interpolants are safe image overapproximations with respect to the property under verification, the trace maintained is safe as well. At each \(i\)-th iteration of standard ITP's inner loop, from the refutation proof of a BMC formula, an overapproximation of the states reachable in \(i\) steps in the system is computed by extracting an interpolant. Such an interpolant is then discarded at the end of the iteration. Furthermore, when a spurious counterexample is found, the current forward traversal is interrupted, the backward cone from the target is unwound by one step and the forward traversal of reachable states restarts once again from the initial states. One of the focus point in IGR is to keep track of the overapproximations computed during each run of ApproxForwardTraversal, in order to enable their reuse in further iterations of the outer loop. It is thus necessary to extend the standard interpolation algorithm to keep track of a _trace_ of reachable states. As the bound \(k\) of the cone increases, stronger overapproximations are computed at each traversed time frame and used to refine the trace. A trace \(\mathbf{F_{k}}=(F_{0},\ldots,F_{k})\) is used in order to keep track of previously computed overapproximations. From Lemma 3, it follows that each timeframe \(F_{i}\) of \(\mathbf{F_{k}}\), with \(0\leq i<k\), is an overapproximation of the set of states that are reachable in exactly \(i\) steps. The trace is constructed so that it is safe with respect to \(P\). The proposed ITP variant, informally called IncrItpModelChecking, is sketched in Algorithms 10 and 11. The differences between the variant and standard interpolation are the following:  
* The trace is initialized with \(F_{0}=\mathcal{I}\) before starting the first forward traversal (Algorithm 10, line 5). * Each time the forward traversal reaches the end of the current trace, a new frame \(F_{i+1}\) is instantiated equal to \(\top\) and added to the trace (Algorithm 11, lines 8-10). * Every time a new interpolant, overapproximating states reachable in \(i+1\) steps, is computed, the corresponding frame \(F_{i+1}\) in the trace is refined (Algorithm 11, lines 17). Refinement is a strengthening step carried out by conjoining the previous set with a new term. ```
1:\(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) a transition system; \(P\) a property over \(V\). 2:\(\langle\mathit{res},\mathit{cex}\rangle\) with \(\mathit{res}\in\{\textsc{Success},\textsc{Fail}\}\); \(\mathit{cex}\) a (possibly empty) initial path representing a counterexample. 3:procedureIncrltpModelChecking(\(\mathcal{M},P\))
4:if\(\exists s_{0}:s_{0}\models\mathcal{I}(V)\wedge\
eg P(V)\)then
5:return\(\langle\textsc{Fail},(s_{0})\rangle\)
6:\(\mathbf{F_{k}}[0]\leftarrow\mathcal{I}\)
7:\(k\gets 1\)
8:while true do
9:\(\langle\mathit{res},\mathit{cex}\rangle\leftarrow\textsc{IncrApproForwardTraversal}( \mathcal{M},P,\mathbf{F_{k}},k)\)
10:if\(\mathit{res}\) is Unreach then
11:return\(\langle\textsc{Success},-\rangle\)
12:elseif\(\mathit{res}\) is Reach then
13:return\(\langle\textsc{Fail},\mathit{cex}\rangle\)
14:\(k\gets k+1\)
```  
**Algorithm 10** Top-level procedure of the proposed ITP variant that keeps track of the computed interpolants using a trace. ```
1:\(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) a transition system; \(P\) a property over \(V\); \(\mathbf{F_{k}}\) a trace; \(k\) bound of a backward unrolling from the target. 2:\(\langle\mathit{res},\mathit{cex}\rangle\) with \(\mathit{res}\in\{\textsc{Reach},\textsc{Unreach},\textsc{Undef}\}\); \(\mathit{cex}\) a (possibly empty) initial path representing a counterexample.