swMATH32310MaRDI QIDQ44021FDOQ44021
Author name not available (Why is that?)
Official website: https://link.springer.com/chapter/10.1007%2F978-3-319-63390-9_7
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
- CVC4SY
- 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
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
This page was built for software: SMTCoq
