[  download | overview | publications | license ]

Download

Please see the README file for installation instructions and release notes.

• Source code: CertCheck 1.0.1.

Overview

Given a QBF input formula F and its certificate C_F generated by QRPcert, CertCheck transforms F into an AIG and merges it with C_F. The resulting AIG is then translated into a propositional formula in CNF, which can be used to validate the correctness of certificate C_F. If the generated CNF is unsatisfiable, C_F is valid and hence represents a valid (counter-)model of F. If the CNF is satisfiable, C_F is invalid.

CertCheck is part of QBFcert, a framework for extracting and validating QBF certificates.

For bug reports etc., please contact Mathias Preiner.

Publications

• Paper and talk at SAT 2012 conference.
• A more detailed description of CertCheck can be found here.

License

CertCheck is developed and maintained by Mathias Preiner.
It is released under GNU GPLv3 (see file COPYING, which is part of the distribution).