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!

winklertobias
Email
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:

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

  • Datenstrukturen und Algorithmen (Vorlesung) SS23

Past semesters

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

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
fulltext PDF [bibtex]
@unpublished{EPIUGF2023,
title = {Exact Probabilistic Inference Using Generating Functions},
author = {Lutz Klinkenberg and Tobias Winkler and Mingshuai Chen and Joost-Pieter Katoen},
type = {Preprint},
year = {2023},
url = { https://publications.rwth-aachen.de/record/862300},
}×
[issue] 		Lutz Klinkenberg, Tobias Winkler, Mingshuai Chen, Joost-Pieter Katoen. Exact Probabilistic Inference Using Generating Functions, 2023.
DOI fulltext PDF [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},
pages = {41 Seiten},
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, 41 Seiten, Springer, 2023.
2022
DOI [bibtex]
@conference{OCRPMCSE2022,
title = {Out of Control: Reducing Probabilistic Models by Control-State Elimination},
author = {Tobias Winkler and Johannes Lehmann and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13182, Theoretical Computer Science and General Issues},
pages = {450-472},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-94583-1_22},
url = { https://publications.rwth-aachen.de/record/838775},
}×
[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.
DOI fulltext PDF [bibtex]
@conference{MCTPRPP2022,
title = {Model Checking Temporal Properties of Recursive Probabilistic Programs},
author = {Tobias Winkler and Christina Gehnen and Joost-Pieter Katoen},
publisher = {Springer},
booktitle = {LNCS},
volume = {13242},
pages = {449-469},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-030-99253-8_23},
url = { https://publications.rwth-aachen.de/record/843600},
}×
[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.
DOI fulltext PDF [bibtex]
@article{W2022,
title = {Weighted programming: a programming paradigm for specifying mathematical models},
author = {Kevin Batz and Adrian Gallus and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Tobias Winkler},
publisher = {ACM},
journal = {Proceedings of the ACM on programming languages},
pages = {pages 66},
type = {Journal Article},
year = {2022},
doi = {10.1145/3527310},
url = { https://publications.rwth-aachen.de/record/845157},
}×
[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.
DOI fulltext PDF [bibtex]
@conference{DPYRDVPPGF2022,
title = {Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions},
author = {Mingshuai Chen and Joost-Pieter Katoen and Lutz Klinkenberg and Tobias Winkler},
publisher = {Springer},
booktitle = {LNCS},
volume = {13371},
pages = {79-101},
type = {Conference Paper},
year = {2022},
doi = {10.1007/978-3-031-13185-1_5},
url = { https://publications.rwth-aachen.de/record/848175},
}×
[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