Progress in Certifying Hardware Model Checking Results

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.

Automated summary

A formal framework was presented to certify k-induction-based model checking results, utilizing the concept of k-witness circuit and a simple inductive invariant. The approach reduces the certification problem to pure SAT checks and checking a simple QBF with one quantifier alternation in order to allow proofs to be checked with an independent proof checker. The resulting certification toolkit CERTIFAIGER was evaluated on instances from the hardware model checking competition, demonstrating the practical use of the certification method.