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-archived

  cvc5

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

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

  BTOR2Tools

A generic parser and tool package for the BTOR2 format.
  https://github.com/boolector/btor2tools

  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