Biography

I am an (interim) associate professor at the Technical University Munich (TUM) at the Campus Heilbronn during the summer semester 2023.

I was Post-Doc at the Institute of Science and Technology Austria (ISTA) / Chatterjee group (2022-2023). I defended my PhD (with distinction) at the Technical University Munich (TUM) under Jan Křetínský (2017-2022). I obtained Masters’ degrees in Math and Computer Science at TUM (both with distinction).

Research

My main research interest is the formal verification of (finite state) probabilistic systems. Currently, I particularly seek to establish a broader recognition for notions of risk in such systems and usage of risk-aware verification.

Aside from that, I contribute to LTL-to-automaton translation, machine learning in verification, complexity theory, and game theory (bidding games & multi agent systems).

Selected Honors, Grants, Awards

• Fellow of the ISTfellow program – 2 year Post-Doc funding
• Nomination for the GI dissertation award 2021 by TUM
• Selected attendee of the 9th Heidelberg Laureate Forum (young researcher)

Selected Publications

Authors sorted alphabetically. Click for a complete list.

Selected Service

Reviews:

• PC member: AAAI (2023), ATVAART (2019), CAV AEC (2022, 2023), TACAS AE (2018, 2019, 2020), HSCC RE (2021, 2022, 2023), PLDI AEC (2023)
• Subreviewer (selection): ATVA, CDC, FORMATS, FoSSaCS, MFCS, VMCAI
• Journals (selection): TCS, STTT, FMSD, IEEE TSE
• Grant agencies: Czech Science Foundation (CZF)
• In total: ~65 reviews so far
• Reviewer for AMS MathSciNet

Co-Organizer of the Young Scientist Symposium 2022 (YSS22)

Teaching

• Developing DOMtutor: A generic library to utilize DOMjudge for teaching (presented at FOMEO’22).
• Designed complete lecture on practical implementation of classical algorithms and data structures using DOMtutor
• Lectured 4 distinct lectures, 7 times TA
• Supervised 3 MSc, 1 BSc Thesis, resulting in two papers

Tools & Libraries

Implementations I am involved in. An asterisk indicates main/sole developer role.

• owl: A library for ω-words, automata, and LTL; state-of-the-art tool for LTL to automaton translations and reactive synthesis (paired with Strix). Homepage and publication.
• Rabinizer 4.0 (*): A tool-set to produce small automata from LTL formulae. Part of Owl. Homepage and publication.
• PET (*): A tool-set to efficiently analyse probabilistic systems using guided sampling. GitLab and publication.
• probabilistic-models (*): A generic, high-performance library to work with finite state probabilistic systems (e.g. Markov decision processes). GitLab.
• JBDD (*): A pure-Java implementation of binary decision diagrams (BDD). GitHub.
• naturals-util (*): A Java library of several utilities for efficiently working with natural numbers (e.g. wrappers for RoaringBitmap). GitHub.
• DOMtutor (*): A library automating interaction with DOMjudge. Homepage and GitHub.

Practical Experience

• Significant contributions to open-source projects, including RoaringBitmap and fastutil
• (Co-)Developer of several major scientific tools and libraries (see above)
• ~3yr FTE at an SMB as CTO, full stack developer for Java (Vaadin, Spring, Hibernate), and embedded systems developer (Raspberry Pi, busybox / buildroot, RAUC, Arduino), project lead for 1-3 developers

Other Interests

• System administration
• (Low-level) hardware engineering (embedded systems, PCB design, soldering, 3D printing)
• Board Games (Go, Scythe, Root, Nemesis, …)
• Digital Games (Baba Is You, Hollow Knight, Pyre, Factorio, Subnautica, …)
• Martial Arts (Black Belt)
• Logic Puzzles (email me if you want to verify your solution idea)