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).
I am one of the developers of our SMT solver Boolector and 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


+43 732 2468 4549 (phone)


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