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 |
|---|---|---|---|
| 2021 March | MSc | Generating invalid C-code using SMT solving | Jana Berger |
| 2020 December | MSc | Investigating Security-related Trees in Storm | Shahid Khan |
| 2020 October | MSc | Probabilistic Inference on Dynamic Bayesian Networks |
Bahare Salmani |
| 2020 May | MSc | On ∞-Safety of Probabilistic Programs | Mingshuai Chen |
| 2020 April | MSc | Linux Kernel – Findings Bugs with Model Checking |
Jana 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 |
Current projects
| Student | Type | Topic | Supervisor |
|---|---|---|---|
| Denis Kuksaus | Master’s Thesis | Verification of Multi-agent Markov Decision Processes |
Tim Quatmann |
| Leon Barth | Bachelor’s Thesis | Compositional Control-Flow Reduction for Probabilistic Model Checking | Tobias Winkler |
| Dario Veltri | Bachelor’s Thesis | Learning MDPs with SMT solving | Joshua Moerman |
| Denise Cassandra Fromme | Master’s Thesis | TBA | Lutz Klinkenberg |
| Hermann Walth | Master’s Thesis | Marking boundaries of fault trees and architectural description languages | Shahid Khan |
| 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 |
| Bram Kohlen | Master’s Thesis | Parameter Synthesis for parametric Probabilistic Timed Automata | Jip Spel |
| Patrick Arens | Bachelor’s Thesis | Extending and applying weakest-preexpectation to (disjoint) concurrent probabilistic progams | Ira Fesefeldt |
| Mohamed Khalifa | Master’s Thesis | Extending a Static Termination Analysis for Heap-Manipulating Programs to Recursion | Ira Fesefeldt |
| Giang Lai | Bachelor’s Thesis | Designing and implementing a graph grammar to model the peano arithmetic | Ira Fesefeldt |
Award Winning Theses
| Student | Topic | Award | Supervisor |
|---|---|---|---|
| Jan Svejda | Interpretation-Based Violation Witness Validator. Master’s Thesis. | DSA Industrial Award (2020) | Philipp Berger |
| Florian Keßler | On the Decidability of Entailment Checking in Quantitative Separation Logics. Bachelor’s Thesis. | Preis der Fachgruppe Informatik der RWTH Aachen für die beste Bachelorarbeit (2020) | Thomas Noll |
| 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
| 2021 | |
|---|---|
| [bibtex] [issue] | Dario Veltri. Learning probabilistic automata with SMT solving, Bachelor Thesis, RWTH Aachen University, 71 Seiten, 2021. |
| [bibtex] [issue] | Mengying Xue, Tim Quatmann. Efficient analysis of time-bounded reachability in markov automata, Master Thesis, RWTH Aachen University, 2021. |
| 2020 | |
| [bibtex] [issue] | . Learning RFSA in Reverse, Bachelor Thesis, RWTH Aachen University, 2020. |
[bibtex]
[issue]
|
. Quantitative Analysis of Counterexample Generation for Automata Learning, Bachelor Thesis, RWTH Aachen University, 2020. |
| [bibtex] [issue] | Christopher Brix. Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds, Master Thesis, RWTH Aachen University, 2020. |
|
[bibtex]
[issue]
|
Linus Heck. Gradient descent on parametric Markov Chains, Bachelor Thesis, RWTH Aachen University, 31 Seiten, 2020. |
|
[bibtex]
[issue]
|
Mohamed Khalifa. Implementation of a Predicate-Guided Termination Analysis for Pointer Programs, Bachelor Thesis, RWTH Aachen University, 2020. |
| [bibtex] [issue] | . RPrIC3, Bachelor Thesis, RWTH Aachen University, 2020. |
| [bibtex] [issue] | Bram Kohlen, Jip Josephine Spel. Parameter synthesis in probabilistic timed automata, Master Thesis, RWTH Aachen University, 91 Seiten, 2020. |
|
[bibtex]
[issue]
|
Daniel Basgöze. Dynamic fault tree analysis using binary decision diagrams, Bachelor Thesis, RWTH Aachen University, 76 Seiten, 2020. |
| [bibtex] [issue] | Lars Beckers, Shahid Khan. A petri net semantics for boolean-logic driven markov processes, Master Thesis, RWTH Aachen University, 55 Seiten, 2020. |
| Show all | |
| 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. |
| Show all | |