Research Scientist, Computer Science
Stanford University
Bitwuzla is a specialized Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions.
https://bitwuzla.github.io
https://github.com/bitwuzla
Boolector is a specialized Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. It further natively handles non-recursive first-order lambda terms.
https://boolector.github.io
https://github.com/boolector/boolector
CVC4 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It supports many theories and their combinations.
https://cvc4.stanford.edu
https://github.com/cvc4/cvc4-archived
cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems and is the successor of CVC4. It supports many theories and their combinations.
https://cvc5.github.io
https://github.com/cvc5/cvc5
ddSMT serves as an input minimizer for Sat Modulo Theories (SMT) benchmarks in SMT-LIB v2 format and its dialects and extensions.
https://ddsmt.readthedocs.io
https://github.com/ddsmt/ddSMT
A generic parser and tool package for the BTOR2 format.
https://github.com/boolector/btor2tools
QBFcert is a framework for resolution-based extraction and validation of certificates for Quantified Boolean Formulas (QBF).
http://fmv.jku.at/qbfcert
QBFDD is a delta-debugger for quantified boolean formulas (QBF) in QDIMACS format.
http://fmv.jku.at/qbfdd
https://github.com/aniemetz/qbfdd
QxBF is a preprocessor for QBFs in QDIMACS format based on failed literal detection.
http://fmv.jku.at/qxbf