If you are interested in writing your master or bachelor thesis in the MOVES group, please contact Prof. Dr. Joost-Pieter Katoen, Prof. Dr. Thomas Noll, or the person indicated with the topics below.
Open topics
| Open since | Type | Topic | Supervisor |
|---|---|---|---|
| Feb 2017 | B | How Fast is Your Modern Probabilistic Model Checker | Sebastian Junges |
| Aug 2017 | B/M | Static state space reduction techniques for MDPs | Sebastian Junges |
Current projects
| Student | Type | Topic | Supervisor |
|---|---|---|---|
| Lutz Klinkenberg | Master’s Thesis | PGF Logics for Probabilistic Programs | Benjamin Kaminski |
| Kevin Batz | Master’s Thesis | TBA | Benjamin Kaminski, Sebastian Junges, Christoph Matheja |
| Sonja Skiba | Bachelor’s Thesis | Towards Complete Proof Rules for Almost-sure Termination of Probabilistic Programs | Benjamin Kaminski |
| David Herzkamp | Bachelor’s Thesis | Hardness of Deciding Termination of Probabilistic Programs with Nondeterminism | Benjamin Kaminski |
| Jan Svejda | Master’s Thesis | Formal Verification of Industrial C Code | Philipp Berger |
| Hannah Arndt | Master’s Thesis | Randomized Meldable Heaps: A more formal proof of a less simple probabilistic data structure | Christoph Matheja |
| Sally Chau | Master’s Thesis | Comparing Hierarchical and On-The-Fly Model Checking for Java Pointer Program | Christoph Matheja |
| Justus Fesefeldt | Master’s Thesis | TBA | Christoph Matheja |
| Philipp Schroer | Bachelor’s Thesis | TBA | Christoph Matheja |
| Bernhard Schulze | Master’s Thesis | TBA | Christoph Matheja |
| Dustin Jungen | Master’s Thesis | SAT-Based Methods for Solving POMDP Problems | Sebastian Junges |
| Sebastian Bartsch | Bachelor’s Thesis | Incremental Scanning (preliminary) |
Thomas Noll |
| Caroline Jabs | Bachelor’s Thesis | Expected Runtimes of Probabilistic Pointer Programs |
Thomas Noll |
| Mirela Mileva | Bachelor’s Thesis | Minimizing Mealy Machines with Dependent Inputs |
Thomas Noll |
| Hannah Mertens | Bachelor’s Thesis | Repairs in Dynamic Fault Trees: a Petri net semantics | Matthias Volk |
| Fynn Mazurkiewicz | Bachelor’s Thesis | Parameter Synthesis for Continuous-Time Markov Chains | Matthias Volk |
Award Winning Theses
| Student | Topic | Award | Supervisor |
|---|---|---|---|
| Lea Hiendl | Human-readable Scheduler Representation for Markov Decision Processes |
Berthold Vöcking Master Award (2018) | Tim Quatmann |
| Clara Scherbaum | Probability Generating Function Semantics for Probabilistic Programs. Bachelor’s Thesis. | itestra innovation Award (2016) |
Benjamin Kaminski |
| Sebastian Junges | Simplifying Dynamic Fault Trees by Graph Rewriting. Master’s Thesis. |
Preis des Fakultätentags Informatik für die beste Masterarbeit (2015) Preis der Fachgruppe Informatik der RWTH Aachen für die beste Masterarbeit (2015) |
Joost-Pieter Katoen |
| Sergey Sazonov | Property Preservation under Bisimulations on Markov Automata. Master’s Thesis. | Preis der Fachgruppe Informatik der RWTH Aachen für die beste Masterarbeit (2014) | Joost-Pieter Katoen |
| Jens Katelaan | Modular Analysis of Concurrent Pointer Programs. Bachelor’s Thesis. | Schönebornpreis (2013) | Thomas Noll |
| Falak Sher | Compositional Abstraction for Probabilistic Automata. Master’s Thesis. | Microsoft Innovation Award (2010) | Joost-Pieter Katoen |
Past projects
| 2019 | |
|---|---|
 | Lukas Westhofen. Verifying Automotive C Code using Modern Software Model Checkers. at RWTH Aachen University, 2019. |
| 2018 | |
| Alexander Bork. Analysing Dynamic Fault Trees by GSPNs. Bachelor Thesis at RWTH Aachen University, 2018. | |
| Sabrina Kowarsch. Modeling and Analysis of a Spacecraft Mission. Master Thesis at RWTH Aachen University, 2018. | |
| Fabian Schneider. A Unified Algebraic Shape Domain. Master Thesis at RWTH Aachen University, 2018. | |
| Lea Hiendl. Human-readable Scheduler Representation for Markov Decision Processes. at RWTH Aachen University, 2018. |
| Felix Bier. From Forest Automata to Hyperedge Replacement Grammars and Back. Master Thesis at RWTH Aachen University, 2018. | |
| Show all | |