My research lies on the boundary between symbolic computation, automated reasoning, and satisfiability checking. Currently I focus on real quantifier elimination, real decision procedures, and reasoning with real arithmetic constraints. Furthermore, I am interested in theories of integers, e.g., Presburger Arithmetic, and their applications.
I have been an active developer of the open-source computer logic system Redlog since 2012.
I am an external expert and associate of the ongoing project H2020-FETOPEN-2015-CSA_712689 SC-Square of the European Union.
Within the SMArT project funded by the ANR and DFG I worked on adaptation of state-of-the-art arithmetic decision procedures for use within an SMT context in order to support formal system verification.
Within the AVACS project funded by the DFG I worked on development and efficient applications of Cylindrical Algebraic Decomposition and Virtual Substitution in the context of non-linear real constraint solving.
- Ph.D. in Computer Science (summa cum laude) at the Saarland University and the Max Planck Institute for Informatics, 2016
- M.Sc. in Computer Science (with honors) at the Comenius University, 2011
- International Max Planck Research School Scholarship, 2011
- Comenius University Rector's award for an outstanding Master's Thesis, 2011
- New Concepts for Real Quantifier Elimination by Virtual
Doctoral Dissertation, Saarland University, 2016.
- Better Answers to Real Questions
(with T. Sturm, A. Dolzmann).
Journal of Symbolic Computation 74:255–275, 2016.
- Constructing a Single Cell in Cylindrical Algebraic Decomposition
(with C. Brown).
Journal of Symbolic Computation 70:14–48, 2015.
- Towards Conflict-Driven Learning for Virtual
Substitution (with K. Korovin, T. Sturm).
CASC 2014, LNCS 8660, pp.256–270, 2014.
- SMT-Based Compiler Support for Memory Access Optimization for
Proceedings of the 5th International Conference on Mathematical Aspects of Computer and System Sciences (MACIS), pp.36–42, 2013.
- Presburger Arithmetic in Memory Access Optimization for
Data-Parallel Languages (with R. Karrenberg, T. Sturm).
FroCoS 2013, LNAI 8152, pp.56–70, 2013.
- Publicity Chair at MACIS 2013
- Reviewer for Journal of Symbolic Computation and Mathematics in Computer Science
- Reviewer at conferences ADG, CASC, ISSAC, LPAR