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 |
|---|---|---|---|
| 2020 April | MSc | Linux Kernel – Findings Bugs with Model Checking |
Philipp Berger |
| 2020 March | MSc | Static Analyses for Probabilistic Model Simplification | Tobias Winkler |
| 2020 February | BSc/MSc | Metrics and Equivalences on formal Power Series for Probabilistic Program Analysis | Lutz Klinkenberg |
| 2020 February | BSc/MSc | Decomposing Probabilistic Program Semantics Computation using Stochastically Independence | Lutz Klinkenberg |
| 2020 February | BSc/MSc | Closed-form Operations on Probability Generating Functions | Lutz Klinkenberg |
| 2020 February | MSc | Existential quantified Graph-Predicates for Hyperedge-Replacement Grammars | Ira Fesefeldt |
| 2019 July | MSc | Learning parametric Markov chains | Joshua Moerman |
| 2019 July | MSc | Quantitative separation logic with presheaves | Joshua Moerman |
| 2019 July | BSc / MSc | Learning MDPs with SMT solving | Joshua Moerman |
Current projects
| Student | Type | Topic | Supervisor |
|---|---|---|---|
| Pascal Pauselli | Bachelor’s Thesis | Theoretical Aspects of Parametric Markov Decision Processes | Tobias Winkler |
| 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 |
| 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 |
| 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 |
| Bram Kohlen | Master’s Thesis | TBA | Jip Spel |
| Mohamed Khalifa | Bachelor’s Thesis | Implementation of a predicate-guided variant search in ATTESTOR | Ira Fesefeldt |
| Dan-Tuong Le | BSc | What is the probability of finding a counterexample? | Joshua Moerman |
| Thomas Vogt | BSc | Duality in Automata Learning II | Joshua Moerman |
| Du Hyun Cho | BSc | Duality in Automata Learning I | 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
| 2020 | |
|---|---|
| Tobias Wirtz. Support for Java Libraries in the Attestor Shape Analysis Tool,. Bachelor Thesis at RWTH Aachen University, 2020. | |
| 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. |
| Lutz Klinkenberg. On Probability Generating Functions for Program Analysis. Master 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 | |