SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
Abstract elided by the publisher.
Related papers
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses CPP 2011
- CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver CAV 2021
- Smt.ml: A Multi-Backend Frontend for SMT Solvers in OCaml TACAS 2026
- Bitwidth customization in image processing pipelines using interval analysis and SMT solvers CC 2020
- Improving Haskell types with SMT Haskell 2015
- Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration OOPSLA 2024
- Deagle: An SMT-based Verifier for Multi-threaded Programs (Competition Contribution) TACAS 2022
- Practical Tactics for Verifying C Programs in Coq CPP 2015