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).
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)
Authors sorted alphabetically. Click for a complete list.
- 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)
- 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.
- 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
- 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)