Certifying Phase Abstraction

Certification helps to increase trust in formal verification ofsafety-critical systems which require assurance on theircorrectness. In hardware model checking, a widely used formalverification technique, phase abstraction is considered one of themost commonly used preprocessing techniques. We present an approachto certify an extended form of phase abstraction using a genericcertificate format. As in earlier works our approach involvesconstructing a witness circuit with an inductive invariant propertythat certifies the correctness of the entire model checking process,which is then validated by an independent certificate checker. Wehave implemented and evaluated the proposed approach includingcertification for various preprocessing configurations on hardwaremodel checking competition benchmarks. As an improvement on previouswork in this area, the proposed method is able to efficientlycomplete certification with an overhead of a fraction of modelchecking time.