Academic Appointments


  • Sr Research Engineer, Computer Science

Professional Education


  • Doctor of Technical Sciences, Johannes Kepler University, Linz (2017)
  • Master of Science, Johannes Kepler University, Linz (2012)
  • Bachelor of Science, Johannes Kepler University, Linz (2010)

All Publications


  • Algorithm selection for SMT MachSMT: Machine Learning Driven Algorithm Selection for SMT Solvers INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER Scott, J., Niemetz, A., Preiner, M., Nejati, S., Ganesh, V. 2023
  • Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers Niemetz, A., Preiner, M., Barrett, C. edited by Shoham, S., Vizel, Y. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 92-106
  • Flexible Proof Production in an Industrial-Strength SMT Solver Barbosa, H., Reynolds, A., Kremer, G., Lachnitt, H., Niemetz, A., Notzli, A., Ozdemir, A., Preiner, M., Viswanathan, A., Viteri, S., Zohar, Y., Tinelli, C., Barrett, C. edited by Blanchette, J., Kovacs, L., Pattinson, D. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 15-35
  • cvc5: A Versatile and Industrial-Strength SMT Solver Barbosa, H., Barrett, C., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., Notzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y. edited by Fisman, D., Rosu, G. SPRINGER INTERNATIONAL PUBLISHING AG. 2022: 415-442
  • Towards Satisfiability Modulo Parametric Bit-vectors JOURNAL OF AUTOMATED REASONING Niemetz, A., Preiner, M., Reynolds, A., Zohar, Y., Barrett, C., Tinelli, C. 2021
  • On solving quantified bit-vector constraints using invertibility conditions FORMAL METHODS IN SYSTEM DESIGN Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C. 2021
  • ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends Kremer, G., Niemetz, A., Preiner, M. edited by Silva, A., Leino, K. R. SPRINGER INTERNATIONAL PUBLISHING AG. 2021: 231-242
  • Invertibility Conditions for Floating-Point Formulas Brain, M., Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C. edited by Dillig, Tasiran, S. SPRINGER INTERNATIONAL PUBLISHING AG. 2019: 116–36
  • Solving Quantified Bit-Vectors Using Invertibility Conditions Niemetz, A., Preiner, M., Reynolds, A., Barrett, C., Tinelli, C. edited by Chockler, H., Weissenbacher, G. SPRINGER INTERNATIONAL PUBLISHING AG. 2018: 236–55
  • BTOR2, BtorMC and Boolector 3.0 Niemetz, A., Preiner, M., Wolf, C., Biere, A. edited by Chockler, H., Weissenbacher, G. SPRINGER INTERNATIONAL PUBLISHING AG. 2018: 587–95