Recent Publications

More Publications

. Btor2 , BtorMC and Boolector 3.0. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I, 2018.

PDF BibTeX DOI Boolector

. Solving Quantified Bit-Vectors Using Invertibility Conditions. Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II, 2018.

PDF BibTeX DOI Extended Version Artifact CVC4

. Rewrites for SMT Solvers using Syntax-Guided Enumeration. Proceedings of the 16th International Workshop on Satisfiability Modulo Theories, SMT 2018), affiliated with the 9th International Joint Conference on Automated Reasoning, IJCAR 2018, Oxford, UK, July 12-13, 2018, 2018.

PDF BibTeX CVC4

. CVC4 at the SMT Competition 2018. CoRR abs/1806.08775, 2018.

PDF BibTeX Arxiv CVC4

. Boolector at the SMT competition 2018. FMV Reports Series, Technical Report 18/1, 2018.

PDF BibTeX Boolector

Recent Talks

More Talks

From Local Search to Quantifier-Elimination for Bit-Vectors in SMT
Aug 31, 2018
Model-Based API Testing for SMT Solvers
Jul 22, 2017

Software / Tools

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.

CVC4

CVC4 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It supports many theories and their combinations.

ddSMT

ddSMT serves as an input minimizer for Sat Modulo Theories (SMT) benchmarks in SMT-LIB v2 format.

QBFcert

QBFcert is a framework for resolution-based extraction and validation of certificates for Quantified Boolean Formulas (QBF).

QBFDD

QBFDD is a delta-debugger for quantified boolean formulas (QBF) in QDIMACS format.

QxBF

QxBF is a preprocessor for QBFs in QDIMACS format based on failed literal detection.

Awards

My work in Boolector contributed to the following awards:

My work in CVC4 contributed to the following awards:

Academic Service

Contact

  • niemetz@cs.stanford.edu
  • Department of Computer Science, Gates 444
    Stanford University
    Stanford, CA 94305