SMTCoq: a plug-in for integrating SMT solvers into Coq

DOI10.1007/978-3-319-63390-9_7zbMath1494.68285OpenAlexW2735882127MaRDI QIDQ2164216

Alain Mebsout, Guy Katz, Clark Barrett, Burak Ekici, Andrew Reynolds, Chantal Keller, Cesare Tinelli

Publication date: 12 August 2022

Full work available at URL: https://doi.org/10.1007/978-3-319-63390-9_7

zbMATH Keywords

satisfiability modulo theoriesproof certificatesexternal solventfunctional arraysZChaff

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (11)

Quantifier simplification by unification in SMT ⋮ Lattice-based refinement in bounded model checking ⋮ Practical Proof Search for Coq by Type Inhabitation ⋮ Unnamed Item ⋮ Primitive Floats in Coq ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ 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 ⋮ Towards bit-width-independent proofs in SMT solvers ⋮ Flexible proof production in an industrial-strength SMT solver

Uses Software

• Coq
• SMTCoq

This page was built for publication: SMTCoq: a plug-in for integrating SMT solvers into Coq