Mathias Preiner

Research Scientist

Stanford University

Biography

Since June 2019 I am a research scientist in Clark Barrett’s group at Stanford University. From 2017-2019 I was a postdoctoral researcher in the same group. I received my Ph.D. in computer science from Johannes Kepler University, supervised by Armin Biere within the National Research Network (NFN) on Rigorous Systems Engineering (RiSE).

Since 2012 I am one of the main developers of the Satisfiability Modulo Theories (SMT) solver Boolector. Since June 2017 I am part of the developer team of the SMT solver CVC4.

My current research interests include developing and improving techniques for solving (quantified) bit-vectors, arrays, as well as improving incremental solving, particularly in the context of word-level model checking applications.

I’m co-organizer of the 2019 edition of the hardware model checking competition HWMCC’19 affiliated to FMCAD’19.

Interests

  • Satisfiability Modulo Theories (SMT)
  • Propositional Satisfiability (SAT)
  • Automated Testing and Debugging Techniques

Education

  • Doctor of Technical Sciences (Dr.techn.) in Computer Science, 2017

    Johannes Kepler University Linz

  • MSc (Dipl.-Ing.) in Computer Science, 2012

    Johannes Kepler University Linz

  • BSc in Computer Sciences, 2010

    Johannes Kepler University Linz

Projects

Boolector

An efficient SMT solver for the theory fixed-size bit-vectors with arrays and uninterpreted functions.

Btor2tools

A generic parser and tool package for the BTOR2 format.

CVC4

An efficient automatic theorem prover for SMT, which supports many different theories and their combination.

QBFcert

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

QxBF

A QBF preprocessor based on failed literal detection.

QBFuzz

A fuzzer for quantified boolean formulas (QBF) in QDIMACS format.

Recent Publications

Boolector at the SMT competition 2019

DRAT-based Bit-Vector Proofs in CVC4

Invertibility Conditions for Floating-Point Formulas

Syntax-Guided Rewrite Rule Enumeration for SMT Solvers

Towards Bit-Width-Independent Proofs in SMT Solvers

Talks

Practical SMT Session (SAT/SMT/AR Summer School 2018)

Counterexample-Guided Model Synthesis

Academic Services

2019

2018

Awards

My work in Boolector and CVC4 contributed to the following awards:

2019

Single Query Track

  • 1st place in division QF_ABV
  • 1st place in division QF_BV

Challenge Track

Model Validation Track

  • 1st place in division QF_BV

Biggest Lead

Largest Contribution

Awards

  • 1 silver trophy for Biggest Lead (Challenge)
  • 2 silver trophies for Largest Contribution (Challenge, Incremental)

Single Query Track

Incremental Track

Unsat Core Track

Biggest Lead

Largest Contribution

Awards

  • 5 gold trophies for Largest Contribution (Single Query, Incremental, Unsat Core)
  • 8 gold trophies for Biggest Lead (Single Query, Incremental, Unsat Core)

2018

Main Track

Application Track

Awards

Main Track

Application Track

Unsat Core Track

Competition-Wide Scoring

Awards

2017

Main Track

2016

Main Track

2015

Main Track

2014

Main Track

  • 1st place in division QF_ABV
  • 1st place in division QF_BV

Awards

Contact