Tobias Winkler

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:

I supervise our research student assistant Adrian Gallus (together with Kevin Batz and Benjamin Kaminski). In the past, I have supervised our student assistants Johannes Lehmann and Christina Gehnen.

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

  • Inference in Probabilistic Programs using Probability Generating Functions (with Lutz Klinkenberg) – Master’s thesis.
  • Conditioning in Recursive Probabilistic Programs (working title) – Master’s thesis.
  • Automatic Entailment Checks for Weighted Programs (working title; with Kevin Batz) – Bachelor’s thesis.
  • Probabilistic Belief Programming (working title; with Alex Bork) – Master’s thesis.

Past thesis projects

  • 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

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)

Publications

You can also find me on dblp and Google Scholar.

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 2022 (FoSSaCS 2022), Volume 13242 of LNCS, 449-469, Springer, 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 = {Theoretical Computer Science and General Issues},
volume = {13182},
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, 23rd International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2022), Volume 13182 of Theoretical Computer Science and General Issues, 450-472, 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.
2021
fulltext PDF [bibtex]
@conference{GFPP2021,
title = {Generating Functions for Probabilistic Programs},
author = {Lutz Klinkenberg and Kevin Batz and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Joshua Moerman and Tobias Winkler},
publisher = {Springer},
booktitle = {Theoretical Computer Science and General Issues},
volume = {12561},
pages = {231-248},
type = {Conference Paper},
year = {2021},
url = { https://publications.rwth-aachen.de/record/807881},
}×
[issue]
Lutz Klinkenberg, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Joshua Moerman, Tobias Winkler. Generating Functions for Probabilistic Programs, 30th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR2020), Volume 12561 of Theoretical Computer Science and General Issues, 231-248, Springer, 2021.
DOI [bibtex]
@article{TM2021,
title = {The complexity of reachability in parametric Markov decision processes},
author = {Sebastian Junges and Joost-Pieter Katoen and Guillermo A. Pérez and Tobias Winkler},
publisher = {Elsevier},
journal = {Journal of computer and system sciences},
volume = {119},
pages = {pages 183-210},
type = {Journal Article},
year = {2021},
doi = {10.1016/j.jcss.2021.02.006},
url = { https://publications.rwth-aachen.de/record/816179},
}×
[issue]
Sebastian Junges, Joost-Pieter Katoen, Guillermo A. Pérez, Tobias Winkler. The complexity of reachability in parametric Markov decision processes, Journal of computer and system sciences 119, pages 183-210, Elsevier, 2021.
DOI arXiv:2109.08317 fulltext PDF [bibtex]
@conference{SGDMO2021,
title = {Stochastic Games with Disjunctions of Multiple Objectives},
author = {Tobias Winkler and Maximilian Weininger},
publisher = {NICTA},
booktitle = {EPTCS},
volume = {346},
pages = {85-100},
type = {Conference Paper},
year = {2021},
doi = {10.4204/EPTCS.346.6},
url = { https://arxiv.org/abs/2109.08317},
}×
[issue]
Tobias Winkler, Maximilian Weininger. Stochastic Games with Disjunctions of Multiple Objectives, 12th International Symposium on Games, Automata, Logics and Formal Verification (GandALF), Volume 346 of EPTCS, 85-100, NICTA, 2021.
Show all