Verified AIG algorithms in ACL2
type: Item
instance of: scholarly article
title: Verified AIG algorithms in ACL2
zbMATH Open document ID: 1542.68095
author: Jared Davis
author: Sol Swords
publication date: 2024-08-13T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68V20
zbMATH DE Number: 7896675
MaRDI profile type: MaRDI publication profile
cites work: A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
cites work: Reconstruction of Z3’s Bit-Vector Proofs in HOL4 and Isabelle/HOL
cites work: Understanding IC3
cites work: Applying Logic Synthesis for Speeding Up SAT
cites work: Theory and Applications of Satisfiability Testing
cites work: LCF-Style Bit-Blasting in HOL4
cites work: Edinburgh LCF. A mechanized logic of computation
cites work: Meta Reasoning in ACL2
cites work: Design and Verification of Microprocessor Systems for High-Assurance Applications
cites work: How can I do that with ACL2? Recent enhancements to ACL2
cites work: Formalization and implementation of modern SAT solvers
cites work: versat: A Verified Modern SAT Solver
cites work: Q5088165
cites work: A Mechanically Verified AIG-to-BDD Conversion Algorithm
cites work: Q5604434
cites work: Efficiently checking propositional refutations in HOL theorem provers
DOI: 10.4204/EPTCS.114.8
description: scientific article; zbMATH DE number 7896675