SMTCoq
From MaRDI portal
Software:44021
swMATH32310MaRDI QIDQ44021FDOQ44021
Author name not available (Why is that?)
Cited In (12)
- Flexible proof production in an industrial-strength SMT solver
- Quantifier simplification by unification in SMT
- Certification of nonclausal connection tableaux proofs
- On solving quantified bit-vector constraints using invertibility conditions
- Towards satisfiability modulo parametric bit-vectors
- Reliable reconstruction of fine-grained proofs in a proof assistant
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- DRAT-based bit-vector proofs in CVC4
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
- Towards bit-width-independent proofs in SMT solvers
- Practical Proof Search for Coq by Type Inhabitation
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for software: SMTCoq
