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 |
|---|---|---|---|
| 2019 July | MSc | Learning parametric Markov chains | Joshua Moerman |
| 2019 July | BSc / MSc | Joshua Moerman | |
| 2019 July | MSc | Quantitative separation logic with presheaves | Joshua Moerman |
| 2019 July | BSc / MSc | Learning MDPs with SMT solving | Joshua Moerman |
| 2019 July | BSc | Joshua Moerman | |
| 2019 Nov | MSc | Monotonicity in MDPs | Jip Spel |
Current projects
| Student | Type | Topic | Supervisor |
|---|---|---|---|
| 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 |
| 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 |
| Tobias Wirtz | Bachelor’s Thesis | Support for Java Libraries in the Attestor Shape Analysis Tool |
Thomas Noll |
| Fynn Mazurkiewicz | Bachelor’s Thesis | Parameter Synthesis for Continuous-Time Markov Chains | Matthias Volk |
| Linus Heck | Bachelor’s Thesis | Gradient Descent for Parametric Markov Chains | Jip Spel and Joshua Moerman |
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 | |
|---|---|
  | Jan Švejda. Interpretation-Based Violation Witness Validator - A novel approach to validation. Master Thesis at RWTH Aachen University, 2019. |
| Paul Lambrich. Precise Long Run Averages for Markov Decision Processes. Bachelor Thesis at RWTH Aachen University, 2019. |
| Sebastian Bartsch. Systematic Design of Efficient Online Scanners. Bachelor Thesis at RWTH Aachen University, 2019. | |
| Mirela Mileva. Minimising Mealy Machines with Dependent Inputs. Bachelor Thesis at RWTH Aachen University, 2019. |
| Hannah Mertens. Repairs in Dynamic Fault Trees: a Petri net semantics. Bachelor Thesis at RWTH Aachen University, 2019. | |
| Caroline Jabs. Expected Runtimes of Probabilistic Pointer Programs. Bachelor Thesis at RWTH Aachen University, 2019. | |
| Lukas Westhofen. Verifying Automotive C Code using Modern Software Model Checkers. Master Thesis at RWTH Aachen University, 2019. |
| Show all | |