  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.
