Pages that link to "Item:Q2164216"
From MaRDI portal
The following pages link to SMTCoq: a plug-in for integrating SMT solvers into Coq (Q2164216):
Displaying 11 items.
- Quantifier simplification by unification in SMT (Q831945) (← links)
- Lattice-based refinement in bounded model checking (Q1629959) (← links)
- On solving quantified bit-vector constraints using invertibility conditions (Q2050109) (← links)
- Towards satisfiability modulo parametric bit-vectors (Q2051567) (← links)
- Reliable reconstruction of fine-grained proofs in a proof assistant (Q2055877) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509) (← links)
- Towards bit-width-independent proofs in SMT solvers (Q2305428) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- Primitive Floats in Coq (Q5875413) (← links)
- (Q5875421) (← links)
