Tobias Winkler | Informatik 2

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

FoSAP SS24

Past semesters

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.

Warning: SQLite3::prepare(): Unable to prepare statement: 5, database is locked in /var/www/html/inc/sqlite-access.php on line 428

Fatal error: Uncaught SQLiteAccessException: Could not prepare statement: REPLACE INTO publications (pub_id, type_id, title, year, pages, publisher, institution, arxiv_id, doi_id, fulltext) VALUES (:pub_id, :type_id, :title, :year, :pages, :publisher, :institution, :arxiv_id, :doi_id, :fulltext); in /var/www/html/inc/sqlite-access.php:433 Stack trace: #0 /var/www/html/inc/sqlite-access.php(64): dbAccess->prepare('REPLACE INTO pu...') #1 /var/www/html/inc/sqlite-access.php(45): dbAccess->prepareStmts() #2 /var/www/html/index.php(73): dbAccess->__construct('/var/www/html/d...', 1) #3 {main} thrown in /var/www/html/inc/sqlite-access.php on line 433