| Alt-Ergo |
Alt-Ergo is an automatic prover of mathematical formulas used behind software verification tools … |
| Bitwuzla |
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … |
| Boolector |
[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … |
| CaDiCaL |
CaDiCaL is a simplified satisfiability solver.
|
| Colibri |
Colibri is an SMT solver.
|
| CryptoMiniSat |
CryptoMiniSat is a SAT solver.
APIs and Bindings This tool is available through the following … |
| cvc4 |
[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … |
| cvc5 |
cvc5 is an automatic theorem prover for SMT problems.
|
| dReal |
[ Not Maintained Since 2023 ] dReal is an automated reasoning tool. It focuses on solving problems … |
| E |
E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with … |
| Glucose |
Glucose is a SAT solver.
|
| Lingeling |
Lingeling is a SAT solver.
|
| MathSAT |
[ Closed-Source Tool ] MiniSat is a minimalistic, open-source SAT solver, developed to help … |
| MiniSat |
[ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … |
| OpenSMT |
OpenSMT is a compact and open-source SMT-solver written in C++, with the main goal of making … |
| ParaFROST |
ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … |
| PRISM |
PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that … |
| Q3B |
[ Not Maintained Since 2023 ] Q3B is an SMT solver for the quantified bit-vector formulas which … |
| Riss |
[ Not Maintained Since 2017 ] Riss is a SAT solving tool collection.
|
| Sally |
Sally is a model checker for infinite state systems described as transition systems.
|
| SMT-RAT |
SMT-RAT is an SMT Real Algebra Toolbox.
APIs and Bindings This tool is available through the … |
| SMTInterpol |
SMTInterpol is an SMT Solver that can compute Craig interpolants for various theories.
APIs and … |
| STAMINA |
A state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces … |
| Storm |
Storm is a tool for the analysis of systems involving random or probabilistic phenomena.
|
| STP |
STP is a constraint solver for quantifier-free bitvectors.
APIs and Bindings This tool is available … |
| Vampire |
Vampire is a theorem prover.
|
| veriT |
veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is … |
| Yices 2 |
Yices is an SMT solver developed by SRI International. It is widely used for checking the … |
| Z3 |
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
APIs and Bindings This … |
| Zipperposition |
Zipperposition is an automated theorem prover for first-order logic with equality and theories.
|