- 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
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] [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. |
[bibtex] [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] [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] [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), 13 Seiten, 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. |
2022 | |
[bibtex] [issue] | Tobias Winkler, Johannes Lehmann, Joost-Pieter Katoen. Out of Control: Reducing Probabilistic Models by Control-State Elimination, 23. International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), Volume 13182, Theoretical Computer Science and General Issues of LNCS, 450-472, Springer, 2022. |
[bibtex] [issue] | Tobias Winkler, Christina Gehnen, Joost-Pieter Katoen. Model Checking Temporal Properties of Recursive Probabilistic Programs, Foundations of Software Science and Computation Structures : 25. International Conference (FOSSACS 2022), Volume 13242 of LNCS, 449-469, Springer, 2022. |
[bibtex] [issue] | Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Tobias Winkler. Weighted programming: a programming paradigm for specifying mathematical models, Proceedings of the ACM on programming languages, pages 66, ACM, 2022. |
[bibtex] [issue] | Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg, Tobias Winkler. Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions, 34. International Conference on Computer Aided Verification (CAV 2022), Volume 13371 of LNCS, 79-101, Springer, 2022. |
2021 | |
[bibtex] [issue] | Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 30. International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2020), Volume 12561 of Theoretical Computer Science and General Issues, 231-248, Springer, 2021. |
[bibtex] [issue] | Joost-Pieter Katoen, , Tobias Winkler. The complexity of reachability in parametric Markov decision processes, Journal of computer and system sciences 119, pages 183-210, Elsevier, 2021. | ,
[bibtex] [issue] | Tobias Winkler, . Stochastic Games with Disjunctions of Multiple Objectives, 12. International Symposium on Games, Automata, Logics and Formal Verification (GandALF), Volume 346 of EPTCS, 85-100, NICTA, 2021. |
2020 | |
[bibtex] [issue] | Joost-Pieter Katoen, , Tobias Winkler. Stochastic Games with Lexicographic Reachability-Safety Objectives, 32. International Conference on Computer Aided Verification (CAV 2020), Volume 12225 of LNCS, 398-420, Springer, 2020. | ,
[bibtex] [issue] | Tobias Winkler. Approximating Values of Generalized-Reachability Stochastic Games, 35. Annual ACM/IEEE Symposium on Logic in Computer Science (LICS '20), ACM conferences, 102-115, Association for Computing Machinery, 2020. | , , , ,
[bibtex] [issue] | Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 2020. https://arxiv.org/abs/2007.06327 |
2019 | |
[bibtex] [issue] | Tobias Winkler, Sebastian Junges, , Joost-Pieter Katoen. On the Complexity of Reachability in Parametric Markov Decision Processes, 30. International Conference on Concurrency Theory (CONCUR), Volume 140 of Leibniz international proceedings in informatics : LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Dagstuhl Publishing, August, 2019. |