Dipl.-Ing. Dr. Mathias Preiner

From June 2012 to April 2017 I was a computer science Ph.D. student within the National Research Network (NFN) on Rigorous Systems Engineering (RiSE), supervised by Prof. Armin Biere at FMV. From April 2017 until June 2017 I continued my research at FMV as a postdoctoral researcher. Since June 2017 I am a postdoctoral scholar at Stanford University working on CVC4 in Clark Barrett's group. I am one of the developers and maintainers of the SMT solver Boolector.

Research Interests

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


A list of my publications can be found here: Publications

Talk Slides


  • Boolector, an SMT solver for bit-vectors and arrays.
  • QRPcert, a tool for extracting Skolem/Herbrand function-based QBF certificates.
  • CertCheck, a tool for validating QBF certificates extracted by QRPcert.
  • QxBF, a QBF preprocessor based on failed literal detection.
  • QBFuzz, a fuzzer for generating random QBF formulae.


My work in boolector contributed to the following awards:


Science Park 3 (SCP3), 2nd Floor
Room S30259




Institute for Formal Models and Verification
Johannes Kepler University
Altenbergerstr. 69
4040 Linz