SMTCoq
From MaRDI portal
Cited in
(22)- 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
- veriT
- CLSAT
- JProver
- tawSolver
- CR-LIBM
- OEuf
- Equations
- CoqHammer
- CnC
- 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
- CVC4SY
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for software: SMTCoq
