Dipl.-Ing. Aina Niemetz

Since June 2012, I am a Computer Science Ph.D. student at FMV, supervised by Prof. Armin Biere.
I am mainly working on improving our SMT solver Boolector.

Research Interests

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

Publications

A list of my publications can be found here: Publications

Talk Slides

Software

  • 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.

Awards

My work in boolector contributed to the following awards:

Office

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

Contact

aina.niemetz@jku.at
+43 732 2468 4549 (phone)

Address

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