Email

tobias.winkler at cs.rwth-aachen.de

Address

Room 4231
Ahornstraße 55
D-52074 Aachen

I am a doctoral researcher and PhD candidate 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 automatic formal verification of discrete 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-Objectives, Temporal Logics, Certificates
• Quantitative Program Analysis: Probabilistic Programs, Weighted Programs, Semi-automatic Loop Verification, Strategy Synthesis, Termination Analysis
• Tool Support for the topics listed above.

I am currently supervising our UnRAVeL research student assistant Samuel Rode. In the past, I have supervised our research student assistants Johannes Lehmann, Christina Gehnen, Adrian Gallus, Tom Biskup, and our DAAD RISE intern Arman Ozcan.

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 contact thesis at i2.informatik.rwth-aachen.de for a general request. I am currently supervising or have supervised the following thesis projects:

Ongoing thesis projects

• An Automata-based Semantics for the Probabilistic ReDiP Language (working title) – Master’s thesis.

Past thesis projects

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

Teaching

Current semester

• FoSAP SS24

Past semesters

• Theoretical Foundations of the UML (Lecture) WS23/24
• Datenstrukturen und Algorithmen (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 (Lecture) SS21
• Probabilistic Programming (Lecture) WS20/21
• Probabilistic Programming (Seminar) WS20/21
• Datenstrukturen und Algorithmen (Vorlesung) SS20
• Introduction to Program Analysis (Proseminar) SS20

Awards

• 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

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

Conferences & Workshops

• 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

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

You can also find me on dblp and Google Scholar.

2024
[bibtex] @article{PSSRNPP2024, title = {Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs}, author = {Kevin Batz and Tom Jannik Biskup and Joost-Pieter Katoen and Tobias Winkler}, publisher = {ACM}, journal = {Proceedings of the ACM on programming languages}, volume = {8}, pages = {pages 93}, type = {Journal Article}, year = {2024}, doi = {10.1145/3632935}, url = { https://publications.rwth-aachen.de/record/979194}, }× [issue]	Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler. Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs, Proceedings of the ACM on programming languages 8, pages 93, ACM, 2024.
[bibtex] @masterthesis{C2024, title = {Complexity and decidability of multi-objective stochastic games}, author = {Tobias Winkler}, publisher = {RWTH Aachen University}, institution = {RWTH Aachen University}, pages = {1 Online-Ressource : Illustrationen}, type = {Master Thesis}, year = {2024}, doi = {10.18154/RWTH-2024-02592}, url = { https://publications.rwth-aachen.de/record/980848}, }× [issue]	Tobias Winkler. Complexity and decidability of multi-objective stochastic games, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
[bibtex] @conference{ACEVTSDMC2024, title = {Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains}, author = {Hannah Mertens and Joost-Pieter Katoen and Tim Quatmann and Tobias Winkler}, publisher = {Springer}, booktitle = {LNCS}, volume = {14571}, pages = {237-257}, type = {Conference Paper}, year = {2024}, doi = {10.1007/978-3-031-57249-4_12}, url = { https://publications.rwth-aachen.de/record/990356}, }× [issue]	Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler. Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains, 30. International Conference TACAS (TACAS 2024), Volume 14571 of LNCS, 237-257, Springer, 2024.
2023
[bibtex] @unpublished{EPIUGF2023, title = {Exact Probabilistic Inference Using Generating Functions}, author = {Lutz Klinkenberg and Tobias Winkler and Mingshuai Chen and Joost-Pieter Katoen}, pages = {3 Seiten}, type = {Preprint}, year = {2023}, doi = {10.48550/arXiv.2302.00513}, url = { https://arxiv.org/abs/2302.00513}, }× [issue]	Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 3 Seiten, 2023. https://arxiv.org/abs/2302.00513
[bibtex] @article{S2023, title = {Stochastic games with lexicographic objectives}, author = {Krishnendu Chatterjee and Joost-Pieter Katoen and Stefanie Mohr and Maximilian Weininger and Tobias Winkler}, publisher = {Springer}, journal = {Formal methods in system design}, volume = {63(1/3)}, pages = {pages 40-80}, type = {Journal Article}, year = {2023}, doi = {10.1007/s10703-023-00411-4}, url = { https://publications.rwth-aachen.de/record/954240}, }× [issue]	Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler. Stochastic games with lexicographic objectives, Formal methods in system design 63 (1/3), pages 40-80, Springer, 2023.
[bibtex] @conference{CPPAOVI2023, title = {Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration}, author = {Tobias Winkler and Joost-Pieter Katoen}, publisher = {Springer}, booktitle = {LNCS}, volume = {13994}, pages = {391-409}, type = {Conference Paper}, year = {2023}, doi = {10.1007/978-3-031-30820-8_24}, url = { https://publications.rwth-aachen.de/record/972636}, }× [issue]	Tobias Winkler, Joost-Pieter Katoen. Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration, 29. International Conference Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023), Volume 13994 of LNCS, 391-409, Springer, 2023.
[bibtex] @conference{OCERTPPA2023, title = {On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata}, author = {Tobias Winkler and Joost-Pieter Katoen}, publisher = {IEEE}, pages = {13 Seiten}, type = {Conference Paper}, year = {2023}, doi = {10.1109/LICS56636.2023.10175714}, url = { https://publications.rwth-aachen.de/record/972664}, }× [issue]	Tobias Winkler, Joost-Pieter Katoen. On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata, 38. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2023), 13 Seiten, IEEE, 2023.
[bibtex] @article{MCTPRPP2023, title = {Model Checking Temporal Properties of Recursive Probabilistic Programs}, author = {Tobias Winkler and Christina Gehnen and Joost-Pieter Katoen}, publisher = {Department of Theoretical Computer Science, Technical University of Braunschweig}, journal = {Logical methods in computer science}, volume = {19(4)}, pages = {pages 24}, type = {Journal Article}, year = {2023}, doi = {10.46298/lmcs-19(4:24)2023}, url = { https://publications.rwth-aachen.de/record/976967}, }× [issue]	Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, Logical methods in computer science 19 (4), pages 24, Department of Theoretical Computer Science, Technical University of Braunschweig, 2023.
Show all