Progress in certifying hardware model checking results

DOI10.1007/978-3-030-81688-9_17zbMATH Open1493.68225OpenAlexW3184346668MaRDI QIDQ832275FDOQ832275

Authors: Emily Yu, Armin Biere, Keijo Heljanko 

Publication date: 25 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-81688-9_17

Recommendations

• scientific article; zbMATH DE number 1798181
• Certifying proofs for SAT-based model checking
• Tools and Algorithms for the Construction and Analysis of Systems
• Efficient verified (UN)SAT certificate checking
• Verified certification of reachability checking for timed automata

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07)

Cites Work

• Computer Aided Verification
• Theory and Applications of Satisfiability Testing
• The existence of refinement mappings
• Temporal induction by incremental SAT solving
• Title not available (Why is that?)
• Equality reasoning in sequent-based calculi
• Certifying proofs for SAT-based model checking
• Non-prenex QBF Solving Using Abstraction
• Horn Clause Solvers for Program Verification
• Title not available (Why is that?)
• Interpolating strong induction

Cited In (4)

• Title not available (Why is that?)
• Model checking: a hardware design perspective
• Word level bitwidth reduction for unbounded hardware model checking
• A methodology for hardware verification using compositional model checking

Uses Software

• MiniSat
• ABC
• Kind 2
• JKind
• AIGER
• CaDiCaL
• Paracooba
• Kissat

This page was built for publication: Progress in certifying hardware model checking results

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q832275)