Model checking is used widely as a formal verification technique for safety-critical systems. Certifying the correctness of model checking results helps increasing confidence in the verification procedure. This can be achieved by additional book-keeping inside existing model checkers. Based on this, we extended an existing BDD-based model checker as well as an IC3-based incremental inductive model checker, to generate certificates during the model checking procedure. We also introduce a proof checker which provides a standardised way to validate certificates generated from model checkers in conjunction with a SAT solver. The main goal is to establish a certification process for the hardware model checking competition.
CITATION STYLE
Yu, Z., Biere, A., & Heljanko, K. (2019). Certifying Hardware Model Checking Results. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11852 LNCS, pp. 498–502). Springer. https://doi.org/10.1007/978-3-030-32409-4_32
Mendeley helps you to discover research relevant for your work.