Email

tobias.winkler at cs.rwth-aachen.de

Address

Room 4231
Ahornstraße 55
D-52074 Aachen

I am a scientific employee and doctoral student in the Software Modeling and Verification Group headed by Professor Joost-Pieter Katoen. Moreover, I am associated with the research training group UnRAVel.

Research

My research focuses on formal verification of probabilistic systems, both from a theoretical and practical point of view. More specifically, my research interests include:

• Probabilistic Model Checking: Probabilistic Pushdown Automata, Markov Decision Processes, Stochastic Games, Multi-Objective Controller Synthesis, Temporal Logics, Certificates
• Quantitative Program Analysis: Probabilistic Programs, Weighted Programs, Quantitative Loop Invariants, Strategy Synthesis, Probability Generating Functions

PhD Thesis

I will defend my PhD thesis titled

Verification and Certification of Probabilistic Recursive Programs via Pushdown Automata

on August 7, 2026. Please feel free to get in touch if you are interested in attending the defense talk.

Thesis Projects

If you are interested in writing a Bachelor/Master’s thesis in any of the areas mentioned above please contact thesis at i2.informatik.rwth-aachen.de for a general request.

Ongoing Thesis Projects

• Belief-Tracking POMDP Policies via Randomized Finite-State Controllers (working title). Bacherlor’s thesis. 2026. (Joint supervision with Lisa Pühl).
• Deciding Finiteness of the Belief Space of Markov Models (working title). Bachelor’s thesis. 2026. (Joint supervision with Alex Bork and Nils Lommen).
• A Zoo of Probabilistic Loops Invariants (working title). Bachelor’s thesis. 2026.

Past Thesis Projects

• Automata-based Semantics for the Probabilistic Programming Language ReDiP – Dominik Geißler, Master’s thesis. 2025.
  Distributional Invariants for Probabilistic Programs – Daniel Zilken, Master’s thesis. 2024. (Joint supervision with Kevin Batz).
• Most Probable Explanations in Bayesian Networks via Weighted Programming – Dinis Vitorino, Bachelor’s thesis. 2024. (Joint supervision with Kevin Batz).
• Model Checking Probabilistic PDA vs Unambiguous Automata – Anastasiia Petrova, Bachelor’s thesis. 2023.
• Invariant-based Strategy Synthesis for Nondeterministic Probabilistic Programs – Tom Biskup, Master’s thesis. 2022. (Joint supervision with Kevin Batz)
  Tom has received the Berthold Vöcking Master Award for his thesis.
• Pushdown and Expectation Transformer Semantics of Probabilistic Recursive Programs with Nested Conditioning – Johannes Lehmann, Master’s thesis. 2022.
• POMDP-based Execution Models for Probabilistic Programs with Partial Observability – Christina Gehnen, Master’s thesis. 2022. (Joint supervision with Alex Bork)
• Automatic Verification of Loop Invariants in Weighted Programs – Ben Sturgis, Bachelor’s thesis. 2022. (Joint supervision with Kevin Batz)
• Inference in Discrete Probabilistic Programs using Probability Generating Functions – Christian Blumenthal, Master’s thesis. 2022. (Joint supervision with Lutz Klinkenberg)
• Implementation of an LTL Model Checker for Probabilistic Pushdown Automata – Laura Bamberger, Bachelor’s thesis. 2022.
• Proving Termination of Probabilistic Recursive Programs via SMT-Solving – Leo Mommers, Bachelor’s thesis. 2022.
• Compositional Control-Flow Reduction for Probabilistic Model Checking – Naomi Barth, Bachelor’s thesis. 2021.
• Automata-based Model Checking of Recursive Systems – Christina Gehnen, Bachelor’s thesis. 2020.
  Christina has received an award from the Fachgruppe Informatik for her thesis.
  

Student Assistants and Interns

In the past, I have supervised our research student assistants Johannes Lehmann, Christina Gehnen, Adrian Gallus, Tom Biskup, Samuel Rode, our DAAD RISE intern Arman Ozcan, and our interns Diane Cauquil (ENS Paris-Saclay) and Ivo Melse (Radboud University).

Teaching

Current Semester

• Static Program Analysis (Lecture) SS26

Past Semesters

• Formale Sprachen, Automaten und Prozesse (“FoSAP”; Vorlesung) SS25
• Formale Sprachen, Automaten und Prozesse (“FoSAP”; Vorlesung) SS24
• Theoretical Foundations of the UML (Lecture) WS23/24
• Datenstrukturen und Algorithmen (“DSAL”; Vorlesung) SS23
• Probabilistic Programming (Lecture) WS22/23
• Probabilistic Programming (Seminar) WS22/23
• Static Program Analysis (Lecture) SS22
• Formal Verification Meets Machine Learning (Seminar) WS21/22
• Modelling and Verification of Probabilistic Systems (“MVPS”; Lecture) SS21
• Probabilistic Programming (Lecture) WS20/21
• Probabilistic Programming (Seminar) WS20/21
• Datenstrukturen und Algorithmen (“DSAL”; Vorlesung) SS20
• Introduction to Program Analysis (Proseminar) SS20

Awards

• Our paper Verifying Sampling Algorithms via Distributional Invariants with Daniel Zilken, Kevin Batz (Cornell), and Joost-Pieter Katoen has received the Best Paper Award at FM 2026.
• Our paper Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops with Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Lutz Klinkenberg won the joint distinguished artifact award of ESOP + FASE + FoSSaCS 2026.
• Our paper Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains with Hannah Mertens, Joost-Pieter Katoen, and Tim Quatmann has received the EAPLS best paper award at ETAPS 2024.
• Our paper Generating Functions for Probabilistic Programs with Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen and Joshua Moerman has received the best paper award at LOPSTR 2020.
• I was awarded the Springorum Medal in 2020 for receiving a master’s degree with distinction.

Peer Review

Journals

• Theoretical Computer Science (TCS) 2026 (reviewer)
• Logical Methods in Computer Science (LMCS) 2022 (reviewer)
• Formal Methods in System Design (FMSD) 2021 (external reviewer)

Conferences & Workshops

• ATVA 2026 (PC member)
• MFCS 2026 (external reviewer)
• LICS 2026 (external reviewer)
• STACS 2026 (external reviewer)
• CONCUR 2025 (external reviewer)
• CAV 2025 (external reviewer)
• TACAS 2025 (external reviewer)
• STACS 2025 (external reviewer)
• IJCAR 2024 (external reviewer)
• CAV 2024 (PC member Artifact Evaluation / external reviewer)
• AAMAS 2024 (external reviewer)
• SODA 2024 (external reviewer)
• MFCS 2023 (external reviewer)
• ATVA 2023 (external reviewer)
• SYNT 2023 @CAV 2023 (PC member)
• POPL 2023 (external reviewer)
• ICTAC 2022 (external reviewer)
• CONCUR 2022 (external reviewer)
• ICALP 2022 (external reviewer)
• LICS 2022 (external reviewer)
• CAV 2022 (PC member Artifact Evaluation / external reviewer)
• POPL 2022 (external reviewer)
• CONCUR 2021 (external reviewer)
• CAV 2021 (PC member Artifact Evaluation / external reviewer)
• FoSSaCS 2021 (external reviewer)

Selected Talks

• Who Verifies the Verifier? Certificates for Probabilistic Model Checking. Workshop talk at UnRAVeL Spring 2025. Aachen, Germany.
• Certifying Positive Almost Sure Termination of Probabilistic Pushdown Automata. Conference talk at Highlights 2024. Bordeaux, France.
• Programmtic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs. Conference talk at POPL 2024. London, UK.
• Probabilistic Language Inclusion Problems. Guest Talk at IMDEA Software Institute, 2023. Madrid, Spain.
• On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata. Conference talk at LICS 2023. Boston, USA.
• Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration. Conference talk at TACAS 2023. Paris, France.
• Model Checking Temporal Properties of Probabilistic Recursive Programs. Conference talk at FoSSaCS 2022. Munich, Germany.
• Out of Control: Reducing Probabilistic Models by Control State Elimination. Conference talk at VMCAI 2022. Philadelphia, USA.
• On the Complexity of Reachability in Parametric MDPs. Conference talk at CONCUR 2019. Amsterdam, The Netherlands.

Publications

See dblp or Google Scholar.