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

Dagstuhl invitation counter: 4

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

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 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: ~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)