PV1 ⊧ Certifaigerchecks whether the result of a k-induction-based model checker is correct

Tool suite for certification of model checking results, independent of any model checker

Application domain/field

• Model checking
• Proof certificates
• Proof checker

Type of tool

Proof certifier/checker

Expected input

• Circuit
• Value $k$ provided by a k-induction-based model checker which outputs a positive model checking result.

Format:

AIGER Note: they extended the reset logic definition of the existing AIGER format to enable reset functions.

Expected output

SUCCESS if the original circuit is safe

Internals

Certifaiger reduces the certification problem to pure SAT checks and checking a simple quantified Boolean formula (QBF) with one quantifier alternation. Uses the SAT solver Kissat for checking validity of the formulas. Uses the QBF solver QuAbS