Progress in certifying hardware model checking results

DOI10.1007/978-3-030-81688-9_17MaRDI QIDQ832275zbMATHOpenAlexFDO

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

Mathematics Subject Classification ID

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

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

Cites work

• scientific article; zbMATH DE number 1796127 (Why is no real title available?)
• scientific article; zbMATH DE number 1798181 (Why is no real title available?)
• Certifying proofs for SAT-based model checking
• Computer Aided Verification
• Equality reasoning in sequent-based calculi
• Horn clause solvers for program verification
• Interpolating strong induction
• Non-prenex QBF solving using abstraction
• Temporal induction by incremental SAT solving
• The existence of refinement mappings
• Theory and Applications of Satisfiability Testing

Cited in

(6)

• Word level bitwidth reduction for unbounded hardware model checking
• A methodology for hardware verification using compositional model checking
• Model checking: a hardware design perspective
• Certifying proofs for SAT-based model checking
• MetaVal: witness validation via verification
• scientific article; zbMATH DE number 2060812 (Why is no real title available?)

Describes a project that uses

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)