# Hardware Model Checking Algorithms and Techniques
## 6 Ic3  
IC3 [48] is a SAT-based algorithm for symbolic invariant verification. Given a transition system \(\mathcal{M}=\langle V,\mathcal{I},T\rangle\) and an invariant property \(P\) over \(V\) to be checked, the target of IC3 is finding an inductive strengthening of \(P\) for \(\mathcal{M}\). In order to carry this out, IC3 maintains two main data structures: a _trace_ and a _proof-obligation queue_. The _trace_\(\mathbf{F_{k}}=(F_{0},\ldots,F_{k})\) is both monotonic and safe with respect to the property \(P\). Each frame \(F_{i}\), with \(0\leq i<k\), is a safe overapproximation of the set of states reachable in at most \(i\) steps in \(\mathcal{M}\) (see Lemmas 4 and 5). The purpose of the algorithm is to iteratively refine such an \(\mathbf{F_{k}}\) in order to satisfy the condition \(F_{i+1}\to F_{i}\) for some \(0\leq i<k\), thus finding an inductive strengthening of \(\psi\) according to Lemma 6. IC3 also maintains a second data structure called a _proof-obligation queue_, which is used to collect sets of states in \(\mathbf{F_{k}}\) that may reach a violation of the property in an arbitrary number of steps. Those sets of states are processed by the algorithm according to a given priority and for each of them IC3 either finds a backward path to the initial states or learns a new inductive lemma that can be used to refine \(\mathbf{F_{k}}\) in order to exclude such states from the overapproximation. In case a path to the initial states is found, the algorithm has found a counterexample to \(P\). In the latter case, the algorithm continues its search of an inductive strengthening of \(P\) over a tighter approximation of the reachable state sets. IC3 needs to solve SAT calls at different stages during its run. Such SAT queries are peculiar [49], in the sense that they are very frequent but involve only a single instance of the transition relation \(T\). Performing many _local reachability checks_, IC3 achieves better control over the precision of the computed overapproximations. Figure 7: Different steps of [PERSON]’s interpolation-based model checking procedure visualized as groupings of states in a transition system \(\mathcal{M}\). States are labeled with their corresponding truth-value assignments to state variables \(V\). States enclosed by solid lines represent the set \(B\) of bad states or states that are backward reachable from a bad state. States enclosed by dotted lines represent the current set \(R\) of states that are reachable from the initial states. States enclosed by dash–dotted lines represent the set \(A\) of states in the image of \(R\). States enclosed by dashed lines represent the interpolant \(I\) that overapproximates \(A\). In (**a**) the initial scenario is depicted, where \(I\) overapproximates the image of \(R\) including both reachable and unreachable states (from \(\mathcal{I}\)). (**b**) depicts the situation after the current set of reachable states \(R\) has been updated by disjoining it with the interpolant \(I\) and the subsequent traversal lead to a spurious counterexample. (**c**) depicts a new traversal after overapproximation refinement. (**d**) depicts the convergence fix-point for the algorithm. Given \(\mathbf{F_{k}}\), each frame \(F_{i}\) is represented by a set of clauses, denoted by clauses \((F_{i})\), to enable efficient syntactic checks for frame equality. The base condition of the trace is fulfilled by initializing the first frame with \(\mathcal{I}\). Monotonicity is maintained syntactically by enforcing the condition clauses\((F_{i+1})\subseteq\text{ clauses}(F_{i})\). On the other hand, image approximation and safety are guaranteed explicitly by the algorithm operations. The main procedure of IC3, described in Algorithm 6, is composed of an initialization phase followed by two nested iterations. During initialization, the algorithm sets up the trace and ensures that the initial states are safe (lines 2-5).