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 16 items.
- Quantifier simplification by unification in SMT (Q831945) (← links)
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver (Q832260) (← links)
- Lattice-based refinement in bounded model checking (Q1629959) (← links)
- Integration of SMT-solvers in B and Event-B development environments (Q1951640) (← 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)
- SMT proof checking using a logical framework (Q2441776) (← links)
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (Q3100209) (← links)
- Practical Proof Search for Coq by Type Inhabitation (Q5048991) (← links)
- Primitive Floats in Coq (Q5875413) (← links)
- (Q5875421) (← links)
- \textsc{Carcara}: an efficient proof checker and elaborator for SMT proofs in the Alethe format (Q6535368) (← links)