Progress in Certifying Hardware Model Checking Results

Abstract We present a formal framework to certifyk-induction-based model checking results. The key idea is the notion of ak-witness circuit which simulates the given circuit and has a simple inductive invariant serving as proof certificate. Our approach allows to check proofs with an independent proof checker by reducing the certification problem to pure SAT checks and checking a simple QBF with one quantifier alternation. We also presentCertifaiger, the resulting certification toolkit, and evaluate it on instances from the hardware model checking competition. Our experiments show the practical use of our certification method.