Tobias Winkler

Email: tobias.winkler at cs.rwth-aachen.de
Address: Room 4231
Ahornstraße 55
D-52074 Aachen
Phone: +49 241 80 21205

I am a postdoctoral researcher 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 have defended my PhD thesis entitled

Verification and Certification of Probabilistic Recursive Programs via Pushdown Automata

on August 7, 2026. The thesis will be published soon.

Bachelor’s and Master’s Theses

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

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.

Publications

2024
DOI	Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler. Stochastic games with lexicographic objectives, 40-80, Springer Science + Business Media B.V, 2024.
DOI	Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs, 93, ACM, 2024.
DOI	Tobias Winkler. Complexity and decidability of multi-objective stochastic games, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI	Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains, Tools and algorithms for the construction and analysis of systems / bernd finkbeiner, laura kovács, editors. - Part 2, 237-257, Springer, 2024.
DOI	Raphael Jean Berthon, Joost-Pieter Katoen, Tobias Winkler. Markov Decision Processes with Sure Parity and Multiple Reachability Objectives, Reachability problems : 18th international conference, RP 2024, vienna, austria, september 25-27, 2024 : proceedings / laura kovács, ana sokolova, editors, 203-220, Springer, 2024.
2023
DOI	Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 3 Seiten, 2023.
DOI	Tobias Winkler, Joost-Pieter Katoen. Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration, Tools and algorithms for the construction and analysis of systems : 29th international conference, TACAS 2023, held as part of the european joint conferences on theory and practice of software, ETAPS 2022, paris, france, april 22–27, 2023, proceedings, part II / edited by sriram sankaranarayanan, natasha sharygina, 391-409, Springer Nature Switzerland, 2023.
DOI	Tobias Winkler, Joost-Pieter Katoen. On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata, 2023 38th annual ACM/IEEE symposium on logic in computer science (LICS) : 26-29 june 2023, boston, USA / conference chair: Marco gaboardi (boston university, USA), 13 Seiten, IEEE, 2023.
DOI	Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, 24, Department of Theoretical Computer Science, Technical University of Braunschweig, 2023.
2022
DOI	Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen. Out of Control : Reducing Probabilistic Models by Control-State Elimination, Verification, model checking, and abstract interpretation : 23rd international conference, VMCAI 2022, philadelphia, PA, USA, january 16–18, 2022, proceedings / edited by bernd finkbeiner, thomas wies, 450-472, Springer, 2022.
DOI	Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, Foundations of software science and computation structures : 25th international conference, FOSSACS 2022, held as part of the european joint conferences on theory and practice of software, ETAPS 2022, munich, germany, april 2–7, 2022, proceedings / edited by patricia bouyer, lutz schröder, 449-469, Springer International Publishing, 2022.
DOI	Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler. Weighted programming : a programming paradigm for specifying mathematical models, 66, ACM, 2022.
DOI	Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler. Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions; 1st ed. 2022., Computer aided verification : 34th international conference, CAV 2022, haifa, israel, august 7–10, 2022, proceedings, part I / edited by sharon shoham, yakir vizel, 79-101, Springer International Publishing, 2022.
2021
DOI	Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, Logic-based program synthesis and transformation : 30th international symposium, LOPSTR 2020, bologna, italy, september 7–9, 2020, proceedings / edited by maribel fernández, 231-248, Springer International Publishing [2021.] ; Cham : Imprint: Springer [2021.], 2021.
DOI	Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, Tobias Winkler. The complexity of reachability in parametric Markov decision processes, 183-210, Elsevier, 2021.
DOI	Tobias Winkler, Maximilian Weininger. Stochastic Games with Disjunctions of Multiple Objectives, Proceedings of the 12th international symposium on games, automata, logics, and formal verification : Padua, italy, 20-22 september 2021 / edited by: Pierre ganty and davide bresolin, 85-100, NICTA, 2021.
2020
DOI	Krishnendu Chatterjee, Joost-Pieter Katoen, Maximilian Weininger, Tobias Winkler. Stochastic Games with Lexicographic Reachability-Safety Objectives, Computer aided verification : 32nd international conference, CAV 2020, los angeles, CA, USA, july 21-24, 2020 : Proceedings, part II / shuvendu K. Lahiri, chao wang (eds), 398-420, Springer, 2020.
DOI	Pranav Ashok, Krishnendu Chatterjee, Jan Křetínský, Maximilian Weininger, Tobias Winkler. Approximating Values of Generalized-Reachability Stochastic Games, Proceedings of the 35th annual ACM/IEEE symposium on logic in computer science (LICS 2020) : July 8-11, 2020, saarbrücken, germany / sponsored by ACM special interest group on logic and computation (SIGLOG), IEEE technical committee on mathematical foundations of computing, association for symbolic logic, european association for theoretical computer science (EATCS) ; conference chairs: Holger hermanns, lijun zhang, naoki kobayashi, 102-115, Association for Computing Machinery, 2020.
DOI	Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 2020.
2019
DOI	Tobias Winkler, Sebastian Junges, Guillermo A. Pérez, Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes, 30th international conference on concurrency theory : CONCUR 2019, august 27-30, 2019, amsterdam, the netherlands / edited by wan fokkink, rob van glabbeek, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August, 2019.