Recent Publications

More Publications

. Propagation based local search for bit-precise reasoning. Formal Methods in System Design, 2017.

Preprint PDF BibTeX DOI Boolector artifact

. Model-Based API Testing for SMT Solvers. Proceedings of the 15th International Workshop on Satisfiability Modulo Theories, SMT 2017, affiliated with the 29th International Conference on Computer Aided Verification, CAV 2017, Heidelberg, Germany, July 24-28, 2017, 2017.

PDF BibTeX Boolector

. Boolector at the SMT competition 2017. 2017.

PDF BibTeX Boolector

. Counterexample-Guided Model Synthesis. Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I, 2017.

PDF BibTeX DOI Boolector artifact

. Bit-Precise Reasoning Beyond Bit-Blasting. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University Linz, 2017.

PDF BibTeX Boolector ddSMT

Recent Talks

More Talks

Model-Based API Testing for SMT Solvers
Jul 22, 2017
Precise and Complete Propagation-Based Local Search for Satisfiability Modulo Theories
Jul 20, 2016

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 (FL).

Awards

My work in Boolector contributed to the following awards:

Academic Service

Contact

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