Dipl.-Ing. Dr. Aina Niemetz

From June 2012 to April 2017 I was a Ph.D. student in Computer Science at FMV, supervised by Prof. Armin Biere within the National Research Network (NFN) on Rigorous Systems Engineering (RiSE). From April 2017 until June 2017 I continued my research at FMV as a postdoctoral researcher. In June 2017 I joined Clark Barret's group as a postdoctoral scholar at Stanford University.
I am one of the developers and maintainers of the SMT solver Boolector and I am now working on the SMT solver CVC4. I am mainly working on quantifier-free bit-vectors.

Research Interests

  • Satisfiability Modulo Theories (SMT)
  • Automated Testing and Debugging Techniques
  • Quantified Boolean Formulas (QBF)
  • SAT


A list of my publications can be found here: Publications

Talk Slides


  • Boolector, an SMT solver for bit-vectors and arrays.
  • ddSMT, a delta debugger for the SMT-LIB v2 format.
  • QRPcheck, a tool for extracting and checking resolution proofs of (un)satisfiability in binary/ascii QRP format.
  • QxBF, a QBF preprocessor based on failed literal detection.
  • QBFDD, a delta-debugger for QBF in QDIMACS format.


My work in Boolector contributed to the following awards:


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




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