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), ATVA (2024), ATVAART (2019), CAV AEC (2022, 2023, 2024), TACAS AE (2018, 2019, 2020), HSCC RE (2021, 2022, 2023, 2024), 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: ~70 reviews so far
- Reviewer for AMS MathSciNet (5 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)