Verified AIG algorithms in ACL2
From MaRDI portal
Publication:6587256
DOI10.4204/EPTCS.114.8zbMATH Open1542.68095MaRDI QIDQ6587256FDOQ6587256
Authors: Jared Davis, Sol Swords 
Publication date: 13 August 2024
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
Specification and verification (program logics, model checking, etc.) (68Q60) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Theory and Applications of Satisfiability Testing
- Edinburgh LCF. A mechanized logic of computation
- Title not available (Why is that?)
- Efficiently checking propositional refutations in HOL theorem provers
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
- Meta Reasoning in ACL2
- Formalization and implementation of modern SAT solvers
- Applying Logic Synthesis for Speeding Up SAT
- Understanding IC3
- versat: A Verified Modern SAT Solver
- LCF-style bit-blasting in HOL4
- Title not available (Why is that?)
- Design and verification of microprocessor systems for high-assurance applications
- A Mechanically Verified AIG-to-BDD Conversion Algorithm
- How can I do that with ACL2? Recent enhancements to ACL2
Cited In (1)
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)
