Matryoshka: Fast Interactive Verification through Strong Higher-Order Automation
SMTCoq | Communication between Coq and SAT/SMT solvers
Haniel Barbosa
Description: An open, trustable and efficinet SMT-solver
theorem prover (4) verit (1) smt solver (1)
veriT is a SMT (Satisfiability Modulo Theories) solver. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and linear arithmetic on real numbers and integers. It also offers good support for quantifiers. The input format is the SMT-LIB 2.0 language and DIMACS .
veriT is open-source and distributed under the BSD license .
veriT has proof-production capabilities that may be used or checked by external tools. At the SMT competition veriT's performance is competitive for some theories.
Matryoshka: Fast Interactive Verification through Strong Higher-Order Automation
SMTCoq | Communication between Coq and SAT/SMT solvers
Haniel Barbosa