Verified AIG algorithms in ACL2
From MaRDI portal
Publication:6587256
Recommendations
- A Mechanically Verified AIG-to-BDD Conversion Algorithm
- Graph-Based Algorithms for Boolean Function Manipulation
- Verification in ACL2 of a generic framework to synthesize SAT-provers
- Simplification in a satisfiability checker for VLSI applications
- Efficient, verified checking of propositional proofs
Cites work
- scientific article; zbMATH DE number 7552936 (Why is no real title available?)
- scientific article; zbMATH DE number 3325539 (Why is no real title available?)
- A Mechanically Verified AIG-to-BDD Conversion Algorithm
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Applying Logic Synthesis for Speeding Up SAT
- Design and verification of microprocessor systems for high-assurance applications
- Edinburgh LCF. A mechanized logic of computation
- Efficiently checking propositional refutations in HOL theorem provers
- Formalization and implementation of modern SAT solvers
- How can I do that with ACL2? Recent enhancements to ACL2
- LCF-style bit-blasting in HOL4
- Meta Reasoning in ACL2
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Theory and Applications of Satisfiability Testing
- Understanding IC3
- versat: A Verified Modern SAT Solver
This page was built for publication: Verified AIG algorithms in ACL2
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6587256)