Certifying Phase Abstraction

TL;DR

This paper introduces a certification method for extended phase abstraction in hardware model checking, using a generic certificate format and witness circuit, improving efficiency and reliability of the verification process.

Contribution

It presents a novel certification approach for extended phase abstraction with a generic certificate format and efficient validation, advancing formal verification trustworthiness.

Findings

Certification completes efficiently with minimal overhead.

The approach successfully certifies various preprocessing configurations.

Implementation on benchmarks demonstrates practical effectiveness.

Abstract

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.