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 July | MSc | Marking boundaries of fault trees and architectural description languages | Shahid Khan |
| 2020 May | MSc | On ∞-Safety of Probabilistic Programs | Mingshuai Chen |
| 2020 April | MSc | Linux Kernel – Findings Bugs with Model Checking |
Philipp Berger |
| 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 |
| 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 (potentially already picked) | Joshua Moerman |
| 2020 July | BSc / MSc | Extending and applying weakest-preexpectation to parallel/concurrent probabilistic progams | Ira Fesefeldt |
Current projects
| Student | Type | Topic | Supervisor |
|---|---|---|---|
| Mengying Xue | Master’s Thesis | Efficient Analysis of Time-bounded Reachability in Markov Automata |
Tim Quatmann |
| Alexander Bork | Master’s Thesis | TBA |
Tim Quatmann |
| Christina Gehnen | Bachelor’s Thesis | TBA | Tobias Winkler |
| Daniel Basgöze | Bachelor’s Thesis | BDD-based analysis of Dynamic Fault Trees | Shahid Khan and Matthias Volk |
| Markus Miliats | Bachelor’s Thesis | Sensitivity Analysis for Dynamic Fault Trees | Matthias Volk |
| Xaver Eugen Fink | Bachelor’s Thesis | Automatically generating and benchmarking case studies for C-code model checking |
Philipp Berger |
| Christopher Brix | Master’s Thesis | Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks using Symbolic Propagation with Error Bounds | Thomas Noll |
| Alexander Hoppen | Master’s Thesis | Design and Implementation of an Interactive Exploration Tool for Probabilistic Programs | Thomas Noll |
| Pascal Pauselli | Bachelor’s Thesis | Theoretical Aspects of Parametric Markov Decision Processes | Tobias Winkler |
| Dustin Jungen | Master’s Thesis | SAT-Based Methods for Solving POMDP Problems | Sebastian Junges |
| Linus Heck | Bachelor’s Thesis | Gradient Descent for Parametric Markov Chains | Jip Spel and Joshua Moerman |
| Bram Kohlen | Master’s Thesis | Parameter Synthesis for parametric Probabilistic Timed Automata | Jip Spel |
| Mohamed Khalifa | Bachelor’s Thesis | Implementation of a predicate-guided variant search in ATTESTOR | Ira Fesefeldt |
| Du Hyun Cho | Bachelor’s Thesis | 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 | Type Theory, Certified Programming and Compiler Verification. 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 | |
|---|---|
[bibtex]
|
. Quantitative Analysis of Counterexample Generation for Automata Learning, Bachelor Thesis, RWTH Aachen University, 2020. |
|
[bibtex]
|
. Learning RFSA in Reverse, Bachelor Thesis, RWTH Aachen University, 2020. |
| 2019 | |
|
[bibtex]
|
Ira Justus Fesefeldt. Proving termination of pointer programs on top of symbolic execution, Master Thesis, RWTH Aachen, pages 118 S., 2019. |
| 2011 | |
|
[bibtex]
|
Gustavo Quirós Araya. Static byte-code analysis for state space reduction, Master Thesis, RWTH Aachen University, pages VIII, 101 S., Publikationsserver der RWTH Aachen University, 2011. |
| 2020 | |
|---|---|
| Florian Keßler. On the Decidability of Entailment Checking in Quantitative Separation Logics. Bachelor Thesis at RWTH Aachen University, 2020. | |
| Tobias Wirtz. Support for Java Libraries in the Attestor Shape Analysis Tool. Bachelor Thesis at RWTH Aachen University, 2020. | |
 | Fynn Mazurkiewicz. Parameter Synthesis for Continuous-Time Markov Chains. 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. |
| Sally Chau. Comparing Hierarchical and On-The-Fly Model Checking for Java Pointer Programs. Master Thesis at RWTH Aachen University, 2019. | |
| Johannes Schulte. Automated Detection and Completion of Confluence for Graph Grammars. 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. |
| Sonja Skiba. Towards Completeness of a Proof Rule for Almost-Sure Termination. Bachelor Thesis at RWTH Aachen University, 2019. | |
| David Herzkamp. Hardness of Probabilistic Termination with Nondeterminism. Bachelor Thesis at RWTH Aachen University, 2019. | |
| Hannah Arndt. Randomized Meldable Heaps: A More Formal Proof of a Less Simple Probabilistic Data Structure. Master Thesis at RWTH Aachen University, 2019. | |
| Philipp Schroer. Understanding Abstraction of Probabilistic 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 | |