Emily Zhengqi Yu, Armin Biere, Keijo Heljanko,
"Progress in Certifying Hardware Model Checking Results"
: Proc. 24rd Computer Aided Verification (CAV'21), Serie Lecture Notes in Computer Science (LNCS), Vol. volume 12760, Springer, Seite(n) 363-386, 7-2021
Progress in Certifying Hardware Model Checking Results
Sprache des Titels:
Proc. 24rd Computer Aided Verification (CAV'21)
We present a formal framework to certifyk-induction-basedmodel checking results. The key idea is the notion of ak-witness circuitwhich simulates the given circuit and has a simple inductive invariantserving as proof certificate. Our approach allows to check proofs with anindependent proof checker by reducing the certification problem to pureSAT checks and checking a simple QBF with one quantifier alternation.We also presentCertifaiger, the resulting certification toolkit, andevaluate it on instances from the hardware model checking competition.Our experiments show the practical use of our certification method.