SMTCoq
From MaRDI portal
Cited in
(22)- veriT
- CLSAT
- 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
- Flexible proof production in an industrial-strength SMT solver
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Certification of nonclausal connection tableaux proofs
- DRAT-based bit-vector proofs in CVC4
- JProver
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- tawSolver
- Towards bit-width-independent proofs in SMT solvers
- CR-LIBM
- OEuf
- Equations
- CoqHammer
- CnC
- Practical Proof Search for Coq by Type Inhabitation
- CVC4SY
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
- Quantifier simplification by unification in SMT
This page was built for software: SMTCoq
