Certifying Phase Abstraction

Certification helps to increase trust in formalverification of safety-critical systems which require assurance ontheir correctness. In hardware model checking, a widely used formalverification technique, phase abstraction is considered one of themost commonly used preprocessing techniques. We present an approachfor certifying 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 model checking results, which isthen validated by an independent certificate checker. We haveimplemented and evaluated the proposed approach includingcertification for various preprocessing configurations on hardwaremodel checking competition benchmarks. As an improvement fromprevious work in this area, the proposed method is able toefficiently complete certification with an overhead of a fraction ofmodel checking time.