I am a Postdoctoral University Assistant in the Forsyte Research Unit at Vienna University of Technology, as well as in the Institute for Symbolic AI at Johannes Kepler University Linz.
My research focuses on solver certification and data extraction from proofs, especially within the context of reasoning without loss of generality in finite domains (SAT/QBF). As of lately I am transitioning into a broader scope including model checking, interactive software verification and untapped use cases for logic-based solvers (specifically, flexible scheduling and procedural content generation). If you are interested in academic collaboration in either of these topics, please send me an email.
The website for our new WWTF-funded project Verifying Without Loss of Generality is now online.
This new WWTF-funded project, directed by myself and Georg Weissenbacher, targets a closer integration between engineer insight and hardware model checking tools through reasoning without loss of generality.
In this paper I present a new proof system that completely bypasses the problems caused by interference in the context of DRAT-like proofs in SAT solving.
I completed my PhD in Computer Science at the Forsyte Research Unit at TU Wien under the supervision of Georg Weissenbacher. As a part of the LogiCS doctoral college, I was also co-supervised by Armin Biere. Previously I got my MSc in Computational Logic from TU Dresden and Free University of Bolzano. I also spent some time at Microsoft Research Cambridge and the lab formerly known as NICTA.
Mailing address: Institute for Computation and Logic, Technische Universität Wien, Favoritenstraße 9-11, 1050 Wien, Austria
Office location: Room HE0316 (3rd floor), Favoritenstraße 11
Email:
Phone: +43-1-58801-740074
Mailing address: Institut für Symbolic Artificial Intelligence, Johannes Kepler Universität Linz, Altenberger Straße 69, 4040 Linz, Austria
Office location: Room 343 (3rd floor), Science Park 4
Email:
Phone: +43 732 2468 5751