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).


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

Selected Publications

Authors sorted alphabetically. Click for a complete list.

Stopping Criteria for Value Iteration on Stochastic Games with Quantitative Objectives
Jan Křetínský, Tobias Meggendorfer, and Maximilian Weininger
LICS 2023
Faster Algorithm for Turn-based Stochastic Games with Bounded Treewidth
SODA 2023
Risk-Aware Stochastic Shortest Path
Tobias Meggendorfer
AAAI 2022
Owl: A Library for ω-Words, Automata, and LTL
Jan Křetínský, Tobias Meggendorfer, and Salomon Sickert
ATVA 2018
Conditional Value-at-Risk for Reachability and Mean Payoff in Markov Decision Processes
Jan Křetínský, and Tobias Meggendorfer
LICS 2018

Selected Service


  • 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.

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)