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

Type of tool

Proof certifier/checker

Expected input

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
Model checking

Links

Source code and data for CAV '21 paper: http://fmv.jku.at/certifaiger/

Related papers

Progress in Certifying Hardware Model Checking Results

Last publication date

15 July 2021

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.