Tobias Winkler

I am currently looking for a student assistant to help developing a Java-based tool for analyzing the termination behavior of programs with recursion and randomness. Feel free to contact me if you are interested!

tobias.winkler at
Room 4231
Ahornstra├če 55
D-52074 Aachen

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


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

In the past, I have supervised our student assistants Johannes Lehmann and Christina Gehnen, and Adrian Gallus.

Thesis projects

If you are interested in writing a Bachelor/Master’s thesis in any of the areas mentioned above, don’t hesitate to contact me. You can also check our list of open topics. I am currently supervising or have supervised the following thesis projects:

Ongoing thesis projects

  • Pushdown and Expectation Transformer Semantics of Probabilistic Recursive Programs with Nested Conditioning – Master’s thesis.
  • Automatic Verification of Loop Invariants in Weighted Programs (with Kevin Batz) – Bachelor’s thesis.
  • POMDP-based Execution Models for Probabilistic Programs with Partial Observability (working title; with Alex Bork) – Master’s thesis.
  • Synthetizing Schedulers from Probabilistic Loop Invariants (working title; with Kevin Batz) – Master’s thesis.

Past thesis projects

  • Inference in Discrete Probabilistic Programs using Probability Generating Functions – Christian Blumenthal, Master’s thesis. 2022.
  • 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 – Leon 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.


Current semester

Past semesters


  • Our paper Generating Functions for Probabilistic Programs (joint work with Kevin Batz, Lutz Klinkenberg, 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



  • FoSSaCS 2021 (external reviewer)
  • CAV 2021 (PC member Artifact Evaluation / external reviewer)
  • CONCUR 2021 (external reviewer)
  • POPL 2022 (external reviewer)
  • CAV 2022 (PC member Artifact Evaluation / external reviewer)
  • LICS 2022 (external reviewer)
  • ICALP 2022 (external reviewer)
  • CONCUR 2022 (external reviewer)
  • ICTAC 2022 (external reviewer)
  • POPL 2023 (external reviewer)


You can also find me on dblp and Google Scholar.