Progress in certifying hardware model checking results

DOI10.1007/978-3-030-81688-9_17zbMath1493.68225OpenAlexW3184346668MaRDI QIDQ832275

Keijo Heljanko, Armin Biere, Emily Yu

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)

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• Certifying proofs for SAT-based model checking
• Non-prenex QBF Solving Using Abstraction
• Horn Clause Solvers for Program Verification
• Computer Aided Verification
• Theory and Applications of Satisfiability Testing
• Interpolating strong induction