Progress in certifying hardware model checking results

DOI10.1007/978-3-030-81688-9_17MaRDI QIDQ832275zbMATH OpenOpenAlexFDO

Authors Emily Yu, Armin Biere, Keijo Heljanko

Publication date 25 March 2022

Copyright license Creative Commons Attribution 4.0 International

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)

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

Describes a project that uses

Uses Software

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

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)