Hardware model checking certification with Certifaiger and Cerbtora

DOI10.1007/978-3-032-32589-1_17MaRDI QIDQ7411171zbMATH OpenFDO

Authors Nils Froleyks, Emily Yu

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32589-1_17

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
• A Practical Approach to Word Level Model Checking of Industrial Netlists
• Bitwuzla
• Certifying phase abstraction
• Clausal congruence closure
• Fast and verified UNSAT certificate checking
• Faster LRAT checking than solving with CaDiCaL
• Handbook of satisfiability. In 2 parts
• scientific article; zbMATH DE number 3325539 (Why is no real title available?)
• Progress in certifying hardware model checking results
• Tools and algorithms for the construction and analysis of systems. 28th international conference, TACAS 2022, held as part of the European joint conferences on theory and practice of software, ETAPS 2022, Munich, Germany, April 2--7, 2022. Proceedings. Pa

This page was built for publication: Hardware model checking certification with Certifaiger and Cerbtora

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