Biography
I am an assistant lecturer at the Lancaster University Leipzig (LUL).
I was an (interim) associate professor at the Technical University Munich (TUM) at the Campus Heilbronn during the summer semester 2023. Before that, 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)
Dagstuhl invitation counter: 4
Selected Publications
Authors sorted alphabetically. Click for a complete list.
Selected Service
Reviews:
- PC (co-)chair: QEST+FORMATS AE 2024
- PC member: AAAI (2023, 2024, 2025), ATVA (2024), ATVAART (2019), CAV AEC (2022, 2023, 2024), TACAS AE (2018, 2019, 2020), HSCC (2025), HSCC RE (2021, 2022, 2023, 2024, 2025), PLDI AEC (2023), RP (2024)
- Subreviewer (selection): ATVA, CDC, FORMATS, FoSSaCS, MFCS, VMCAI
- Journals (selection): TCS, STTT, FMSD, IEEE TSE
- Grant agencies: Czech Science Foundation (CZF)
- In total: ~80 reviews so far
- Reviewer for AMS MathSciNet (6 reviews)
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 5 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 and SemML below). Homepage and publication.
- Rabinizer 4.0 (*): A tool-set to produce small automata from LTL formulae. Part of Owl. Homepage and publication.
- SemML: Semantic Machine Learning for LTL reactive synthesis. Use ML guidance to improve synthesis. Based on Owl. Winner of SYNTCOMP 2024 LTL Realizability Track.
- PET (*): A tool-set to efficiently analyse probabilistic systems using guided sampling. GitLab and publication (previous).
- probabilistic-models (*): A generic, high-performance library to work with finite state probabilistic systems (e.g. Markov decision processes). GitLab.
- JBDD (*): A pure-Java, high-performance implementation of (reduced, ordered) binary decision diagrams (ROBDD). 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, fastutil, and benchexec
- (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)