Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered one of the most commonly used preprocessing techniques. We present an approach to certify an extended form of phase abstraction using a generic certificate format. As in earlier works our approach involves constructing a witness circuit with an inductive invariant property that certifies the correctness of the entire model checking process, which is then validated by an independent certificate checker. We have implemented and evaluated the proposed approach including certification for various preprocessing configurations on hardware model checking competition benchmarks. As an improvement on previous work in this area, the proposed method is able to efficiently complete certification with an overhead of a fraction of model checking time.

翻译：认证有助于增强对安全关键系统形式化验证的信任，此类系统需要保证其正确性。在硬件模型检测（一种广泛使用的形式化验证技术）中，相位抽象被认为是最常用的预处理技术之一。我们提出了一种方法，利用通用证书格式对扩展形式的相位抽象进行认证。与以往工作类似，我们的方法包括构建一个具有归纳不变性属性的见证电路，该属性可验证整个模型检测过程的正确性，随后由独立的证书检查器进行验证。我们已在硬件模型检测竞赛基准上对所提方法进行了实现与评估，涵盖各种预处理配置下的认证。作为对该领域先前工作的改进，本方法能够高效完成认证，其额外开销仅为模型检测时间的一小部分。