Verified AIG algorithms in ACL2
From MaRDI portal
Publication:6587256
DOI10.4204/eptcs.114.8zbMATH Open1542.68095MaRDI QIDQ6587256
Publication date: 13 August 2024
Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Unnamed Item
- Unnamed Item
- Formalization and implementation of modern SAT solvers
- Efficiently checking propositional refutations in HOL theorem provers
- Edinburgh LCF. A mechanized logic of computation
- Understanding IC3
- versat: A Verified Modern SAT Solver
- LCF-Style Bit-Blasting in HOL4
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
- Applying Logic Synthesis for Speeding Up SAT
- Design and Verification of Microprocessor Systems for High-Assurance Applications
- Theory and Applications of Satisfiability Testing
- Meta Reasoning in ACL2
- A Mechanically Verified AIG-to-BDD Conversion Algorithm
- How can I do that with ACL2? Recent enhancements to ACL2
This page was built for publication: Verified AIG algorithms in ACL2
