Aina Niemetz

Research Scientist, Computer Science
Stanford University

           

Publications
Talks
Tools
Awards

Tools

  Bitwuzla

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

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

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

  ddSMT

ddSMT serves as an input minimizer for Sat Modulo Theories (SMT) benchmarks in SMT-LIB v2 format.
  https://github.com/aniemetz/ddSMT

  QBFcert

QBFcert is a framework for resolution-based extraction and validation of certificates for Quantified Boolean Formulas (QBF).
  http://fmv.jku.at/qbfcert

  QBFDD

QBFDD is a delta-debugger for quantified boolean formulas (QBF) in QDIMACS format.
  http://fmv.jku.at/qbfdd
  https://github.com/aniemetz/qbfdd

  QxBF

QxBF is a preprocessor for QBFs in QDIMACS format based on failed literal detection.
  http://fmv.jku.at/qxbf