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 cs.rwth-aachen.de
- Address
- 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.
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.
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
- Model Checking Probabilistic PDA against Unambiguous Automata (working title) – Bachelor’s thesis.
Past thesis projects
- Invariant-based Strategy Synthesis for Nondeterministic Probabilistic Programs – Tom Biskup, Master’s thesis. 2022. (Joint supervision with Kevin Batz)
- 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 – 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.
Teaching
Current semester
Past semesters
- Static Program Analysis SS22
- Formal Verification Meets Machine Learning (Seminar) WS21/22
- Modelling and Verification of Probabilistic Systems SS21
- Probabilistic Programming WS20/21
- Probabilistic Programming (Seminar) WS20/21
- Datenstrukturen und Algorithmen 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
- Formal Methods in System Design (FMSD) 2021 (external reviewer)
- Logical Methods in Computer Science (LMCS) 2022 (reviewer)
Conferences
- 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)
Publications
You can also find me on dblp and Google Scholar.
| 2023 | |
|---|---|
[bibtex]
[issue]
|
Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 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. |
| Show all | |