k-归纳模型检测结果的认证器

A Certifier for k-Induction Model Checking Results

摘要: 基于k-归纳的模型检测可以验证许多重要的系统，但在具体的实现过程中仍可能存在缺陷，所以对其结果进行认证是非常必要的。目前最有效的方法是利用k-证据电路的概念扩展给定的模型检测问题，然后使用认证器进行判定，但是在部分情况下，QBF的验证大大增加了认证时间。为了解决这一问题，本文提出对复位检测的算法进行优化，创建了一个新的复位条件并添加了带映射的原始电路来减小QBF。并且本文还使用C语言实现了认证器。实验结果表明：利用优化算法生成的QBF有效减少了认证时间，利用C语言实现的认证器也为之后的研究提供了有力工具。

Abstract: Model checking based on k-induction can verify many important systems, but there may still be de-fects in the implementation process, so it is very necessary to verify the results. At present, the most effective method is to extend the given model checking problem by using the concept of k-witness circuit, and then use the certifier to determine. However, in some cases, the verification of QBF greatly increases the certification time. In order to solve this problem, this paper proposes to opti-mize the reset checking algorithm, create a new reset condition and add the original circuit with mapping to reduce QBF. And this paper also uses C language to achieve the certification. The ex-perimental results show that the QBF generated by the optimization algorithm effectively reduces the certification time, and the certifier implemented by C language also provides a powerful tool for future research.