# Hardware Model Checking Algorithms and Techniques
## 5 Interpolation-Based Model Checking
### [PERSON]'s Interpolation Algorithm
Otherwise, \(A\wedge B\) is Unsat and an interpolant \(I\) can be derived from its refutation proof (line 11). Such an interpolant represents a safe overapproximation of the states reachable from \(R\) in one transition with respect to the bad cone \(Cone(1,k)\), as illustrated in Figure 6. Therefore, no counterexample can be reached from \(I\) in \(k-1\) or less transitions, i.e., \(I\) is safe with respect to \(P\). Since the interpolant is an overapproximation of the image of \(R\), it is treated as a _candidate inductive invariant_. The algorithm checks whether consecution \(I\to R\) is valid (i.e., \(\
eg R\wedge I\) is unsatisfiable). In that case, \(R\) is an inductive invariant for \(\mathcal{M}\) and, since \(R\) is safe with respect to \(P\), it is also an inductive strengthening for \(P\). Conversely, a new set of overapproximated forward reachable states is computed as \(R\lor I\) and the algorithm iterates once again. The result of the nested procedure, i.e., the sequence of \(R\) composed at each iteration, can be seen as a safe monotonic trace. Monotonicity stems from having \(R\) initialized with \(\mathcal{I}\) (line 2) and from the fact that each consecutive \(R\) is a disjunction of the previous one and of an overapproximation of the states reachable from the previous (line 14). Safety with respect to \(P\) stems from the fact that \(\mathcal{I}\) was proved to be safe (Algorithm 4, lines 2-4) and taking into the account that each interpolant \(I\) used to construct \(R\) does not intersect \(Cone(1,k)\). From Lemma 7 follows the detection of an inductive strengthening for \(P\) from that trace. The sequence of interpolants, instead, can be seen as a non-monotonic safe trace. Taking into account Algorithm 4, in the beginning, the initial states \(\mathcal{I}\) are checked to be safe (line 2-3). If said check fails, there exists a trivial counterexample consisting of just a single initial state. The procedure can then halt and return the counterexample found. Conversely, the bad cone bound \(k\) is initialized to 1 (line 4) and the procedure starts iterating forward overapproximated traversals of reachable states, while keeping safety with respect to a bad cone of increasing depth \(k\) from the target (lines 5-11). Increasing the value of \(k\) lets the algorithm find real counterexamples and generate more precise overapproximations on subsequent iterations. Since the bad cone from the target unwinds, a few states in the overapproximated images computed at previous iterations might be reached by the unrolling and are therefore excluded from newer images. During each outer loop iteration, the inner procedure starts a forward traversal from scratch from the initial states. As \(k\) increases, the algorithm is guaranteed to find a bound \(k\) in which the computed interpolants are precise enough to find an inductive strengthening if \(P\) holds for the system, or to find a real counterexample otherwise [44]. Figure 6: Interpolation as an overapproximated image operator. Interpolant \(I\) is an overapproximation of the image of \(R\) that does not intersect \(Cone(1,k)\).