veriT
From MaRDI portal
VeriT
Cited in
(67)- Goeland
- SMT-LIB
- libpoly
- Positive solutions of systems of signed parametric polynomial inequalities
- GiNaCRA
- Zenon
- SMTInterpol
- Integration of SMT-solvers in B and Event-B development environments
- CVC Lite
- A superposition calculus for abductive reasoning
- CLSAT
- OpenSMT
- Reliable reconstruction of fine-grained proofs in a proof assistant
- CPGraph
- Flexible proof production in an industrial-strength SMT solver
- Cooperating techniques for solving nonlinear real arithmetic in the \texttt{cvc5} SMT solver (system description)
- CERES
- CVC4
- MathSAT5
- Extending SMT solvers to higher-order logic
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Modular strategic SMT solving with \textbf{SMT-RAT}
- SMT proof checking using a logical framework
- SMT-RAT
- Hadamard
- MathCheck
- Lynx
- Beagle
- raSAT
- \textsf{SC}\(^2\): satisfiability checking meets symbolic computation. (Project paper)
- Building bridges between symbolic computation and satisfiability checking
- MathCheck2: A SAT+CAS Verifier for Combinatorial Conjectures
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Compression of propositional resolution proofs by lowering subproofs
- Decision procedures for flat array properties
- Semi-intelligible Isar proofs from machine-generated proofs
- versat: A Verified Modern SAT Solver
- A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
- Modular SMT proofs for fast reflexive checking inside Coq
- TIP
- Satisfiability modulo theories
- SageSAT
- nsoks
- Congruence closure with free variables
- Saturate
- A learning-based fact selector for Isabelle/HOL
- GAPT
- MathCheck: a math assistant via a combination of computer algebra systems and SAT solvers
- Scavenger
- Psyche
- iSAT
- CoqHammer
- FLOTTER
- Combining decision procedures by (model-)equality propagation
- SMTCoq
- A Meta-level Annotation Language for Legal Texts
- Towards an Executable Methodology for the Formalization of Legal Texts
- Exploiting symmetry in SMT problems
- Compression of propositional resolution proofs via partial regularization
- scientific article; zbMATH DE number 7178358 (Why is no real title available?)
- Complexity of translations from resolution to sequent calculus
- egg
- Ordered_Resolution_Prover
- Scalable fine-grained proofs for formula processing
- CertiStr
- Zephyrus2
- Quantifier simplification by unification in SMT
This page was built for software: veriT
