Progress in Certifying Hardware Model Checking Results

Abstract

Abstract We present a formal framework to certify k -induction-based model checking results. The key idea is the notion of a k -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 present Certifaiger , 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.

Topics & Concepts