一句话：提出复用不可满足核心与可满足模型的 IC3 验证加速方法，显著减少求解器调用并提速。
IC3 是模型检测的重要突破，但验证复杂程序时依赖大量且频繁的约束求解调用，效率受限。作者观察到 IC3 中许多约束具有相似性，因而提出通过复用先前约束的不可满足核心（unsatisfiable core）和可满足模型（satisfying model）来加速验证。方法构建不可满足核心库（UCL）与可满足模型库（SML），存储并索引验证过程中生成的关键核心和模型；当收到新的约束求解请求时，先利用已有核心和模型预判约束可满足性，从而减少实际求解器调用。作者在 Kind2 上实现该方法，并在 Kind2 标准基准集上评估。实验表明，在复杂样例上求解器调用次数可减少一个数量级，取得 4.35 倍加速，同时内存消耗更低。
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.
@inproceedings{paperbot11890,
title = {Accelerating IC3 Verification by Exploiting Unsatisfiable Cores and Satisfying Models},
author = {Xinyi Gong and Liangze Yin and Yuhan Li and Ke Kang and Wei Dong and Shanshan Li and Ji Wang},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3787819}
}