- 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 analysis of discrete probabilistic systems, both from a theoretical and practical point of view. More specifically, my research interests include:
- Probabilistic Model Checking, in particular termination analysis and temporal properties of probabilistic pushdown systems, stochastic games with multiple objectives, general state-space reduction techniques, and parametric Markov models.
- Probabilistic Programs, in particular calculi for verifying potentially unbounded while-loops in probabilistic integer programs. More recently, my co-authors and me have studied more general Weighted Programs.
- 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
- Distributional Invariants for Probabilistic Programs (working title) – Master’s thesis. (Joint supervision with Kevin Batz).
Past thesis projects
- 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
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 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
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]
[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]
[issue]
|
Tobias Winkler. Complexity and decidability of multi-objective stochastic games, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024. |
| 2023 | |
|
[bibtex]
[issue]
|
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 2023. |
|
[bibtex]
[issue]
|
Krishnendu Chatterjee, Joost-Pieter Katoen, Stefanie Mohr, Maximilian Weininger, Tobias Winkler. Stochastic games with lexicographic objectives, Formal methods in system design, 41 Seiten, Springer, 2023. |
|
[bibtex]
[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]
[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), IEEE, 2023. |
|
[bibtex]
[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 | |