Glucose SAT Solver
Glucose is a SAT solver.
GlucoseWelcome to this collection of Formal Methods Tools, which aims to be the world’s most comprehensive source for information on tools for formal methods. From decades-old classics to cutting-edge tools, this site aims to put as much information as possible into one convenient place. Explore a wide selection of tools, contribute tools you make or love, and help grow the formal methods community.
Below are some quick links that may be helpful, plus a random selection of tools (refreshed every time I push updates to this site).
This list shows a selection of 20 random tools, refreshed every time this site is updated.
Glucose is a SAT solver.
GlucoseCryptoMiniSat is a SAT solver. APIs and Bindings This tool is available through the following interfaces: C++ Namespace: …
CryptoMiniSatColibri is an SMT solver.
ColibriSMT-RAT is an SMT Real Algebra Toolbox. APIs and Bindings This tool is available through the following interfaces: C++ API: …
SMT-RATPRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or …
PRISMSally is a model checker for infinite state systems described as transition systems.
SallySMTInterpol is an SMT Solver that can compute Craig interpolants for various theories. APIs and Bindings This tool is …
SMTInterpol[ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help researchers and …
MiniSatcvc5 is an automatic theorem prover for SMT problems.
cvc5Z3 is a general-purpose theorem prover widely used for SAT & SMT solving. APIs and Bindings This tool is available …
Z3[ Not Maintained Since 2017 ] Riss is a SAT solving tool collection.
Riss[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size …
Boolector[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded by cvc5
cvc4Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point …
BitwuzlaParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA CUDA-enabled GPUs in …
ParaFROSTA state-space truncation tool for Markov-Chains that can analyze infinite-sized models. Intefaces with either Storm or PRISM. …
STAMINAYices is an SMT solver developed by SRI International. It is widely used for checking the satisfiability of logical formulas …
Yices 2STP is a constraint solver for quantifier-free bitvectors. APIs and Bindings This tool is available through the following …
STPLingeling is a SAT solver.
LingelingveriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is designed for use in formal …
veriT