Accelerating IC3 Verification by Exploiting Unsatisfiable Cores and Satisfying Models

The IC3 algorithm represents a groundbreaking advancement in the field of model checking. However, its heavy reliance on numerous and frequent constraint-solving calls poses significant challenges when verifying complex programs. We observe that many of the constraints solved within IC3 share remarkable similarities. Based on this observation, we propose an IC3 acceleration verification method by reusing unsatisfiable cores and satisfying models of previous constraints. This method constructs an Unsatisfiable Core Library (UCL) and a Satisfying Model Library (SML) to store and index crucial unsatisfiable cores and satisfying models generated during the verification process. When a new constraint-solving request is received, our method preemptively determines the satisfiability of the constraint using the existing unsatisfiable cores and satisfying models. This approach can significantly reduce the number of required solver calls, thereby enhancing the verification efficiency. We have implemented our method on Kind2 and evaluated it on the standard benchmark suite of Kind2. Experimental evaluation demonstrates that, for complex examples, our method can reduce the number of solver calls by an order of magnitude, and achieves a 4.35-fold speedup with even less memory consumption.