A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
No abstract available.
Related papers
- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver CAV 2021
- SMTCoq: A Plug-In for Integrating SMT Solvers into Coq CAV 2017
- Modular SMT Proofs for Fast Reflexive Checking Inside Coq CPP 2011
- DRAT Proofs of Unsatisfiability for SAT Modulo Monotonic Theories TACAS 2024
- The Proof Complexity of SMT Solvers CAV 2018
- Clausal Proofs for Pseudo-Boolean Reasoning TACAS 2022
- Orbitopal Fixing in SAT TACAS 2026
- Z3-Noodler 1.3: Shepherding Decision Procedures for Strings with Model Generation TACAS 2025