SMT
Bitwuzla
SMT Solver
Bitwuzla is an award-winning Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations.
View on GitHub
Boolector
SMT Solver
Boolector is an award-winning Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions and their combinations.
View on GitHub
cvc5
SMT Solver
cvc5 is an award-winning automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. cvc5 is the successor of CVC4.
View on GitHub
ddsmt
Delta Debugger for SMT-LIB
ddSMT is a delta debugger for input in the SMT-LIB language and its dialects and extensions. It serves as an input minimizer for SMT-LIB(-like) input that triggers interesting behavior for a given command.
View on GitHub
Murxla
An API Fuzzer for SMT Solvers
Murxla is a solver-agnostic fuzzer for SMT Solvers that randomly generates valid sequences of solver API calls based on a customizable API model, with full support for semantics and features of SMT-LIB.
View on GitHub
Smt-Switch
A Solver-Agnostic C++ API for SMT Solving
Smt-Switch provides abstract C++ classes which can be implemented by different SMT solvers. Our model checker Pono is built using Smt-Switch.
View on GitHub
Model Checking
Pono
SMT-Based Model Checker
Pono is a flexible and extensible SMT-based model checker that leverages word-level reasoning. 'Pono' is the Hawaiian word for proper, correct, or goodness.
Pono is the successor of our model checkers CoSA and CoSA2.
View on GitHub
Pono is the successor of our model checkers CoSA and CoSA2.
Neural Network Verification
Marabou
SMT-Based Framework for Verifying Deep Neural Networks
Marabou is an SMT-based tool that can answer queries about the properties of a neural network by transforming these queries into constraint satisfaction problems.
View on GitHub
Deprecated Tools
Cosa
CoreIR Symbolic Analyzer
CoSA is an SMT-based symbolic model checker for hardware designs. It is succeeded by Pono.
View on GitHub
Cosa2
CoreIR Symbolic Analyzer
CoSA2 is an SMT-based symbolic model checker for hardware designs. It is succeeded by Pono.
View on GitHub
CVC4
SMT Solver
CVC4 is an award-winning automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It is succeeded by cvc5.
View on GitHub