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

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. 2025. (Joint supervision with Alex Bork and Nils Lommen).

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