Competitions
Several prizes won in QBF competition tracks with the QBF solver DepQBF and related tools, jointly with my co-authors:
- Medal (first place) in QBFEVAL 2018 solver competition, part of FLoC Olympic Games.
- Kurt Gödel Society medal in the QBF Gallery 2014, part of FLoC Olympic Games. TU Wien news article (in German).
- First place in QBFEVAL 2017 solver competition.
- First place in QBFEVAL 2012 solver competition.
- First place in QBFEVAL 2010 solver competition.
- Two second places in the QBFEVAL 2020 solver competition.
- Second place in the QBFEVAL 2019 solver competition.
- Two second places and one third place in the QBFEVAL 2018 solver competition.
- Two silver and one bronze medal in the QBF Gallery 2014, part of FLoC Olympic Games.
- Two third places in the QBFEVAL 2016 solver competition.
Further Awards
- FLoC Olympic Games 2026: QBFGallery 2026 Test-of-Time Award, jointly with Armin Biere and Uwe Egly, for outstanding contributions to QBF solver development, search-based solver DepQBF, proof systems, and practical solving techniques.
- Runner-up of the Heinz Zemanek Dissertation Award 2016 of the Austrian Computer Society.
- Reward check from Donald Knuth for a comment on his book The Art of Computer Programming, Volume 4, Fascicle 6: “Satisfiability”.
- Winner of the 2019 IJCAI-JAIR Best Paper Prize for our paper Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. 53: 127-168 (2015), jointly with Marijn Heule, Matti Järvisalo, Martina Seidl, and Armin Biere.
- Honorable Mention for our paper A Theoretical Framework for Symbolic Quick Error Detection at Formal Methods in Computer-Aided Design (FMCAD) 2020 conference, jointly with Clark Barrett and Subhasish Mitra.
- Best Tool Paper Award for our paper Pono 2.0: A Versatile SMT-Based Model Checker for Safety and Liveness, at the International Symposium on Formal Methods (FM 2026), jointly with Áron Ricardo Perez-Lopez, Po-Chun Chien, Samantha Archer, Ahmed Irfan and Clark Barrett.
- Best paper nomination for our paper Lightweight Online Learning for Sets of Related Problems in Automated Reasoning, at Formal Methods in Computer-Aided Design (FMCAD) 2023 conference, jointly with Haoze Wu, Christopher Hahn, Makai Mann, Raghuram Ramanujan, and Clark Barrett.
- Invited commentary on our paper Evaluating QBF Solvers: Quantifier Alternations Matter published at the International Conference on Principles and Practice of Constraint Programming (CP) 2018, on the occasion of the 25th edition of CP, jointly with Uwe Egly.
- Winner of the Oski Award with the model checker CoSA2 (now called Pono) in the Hardware Model Checking Competition 2019, jointly with Makai Mann, Ahmed Irfan, and Clark Barrett.
- Best student paper award at the Bit-Precise Reasoning Workshop 2008, jointly with Robert Brummayer.