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 December | MSc | Investigating Security-related Trees in Storm | Shahid Khan |
2020 December | BSc | Computing loop-representative states as efficiently as possible (maybe taken) |
Ira Fesefeldt |
2020 October | MSc | Probabilistic Inference on Dynamic Bayesian Networks |
Bahare Salmani |
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 |
2020 Nov | BSc/MSc | Probabilistic Model Reduction by Control-State Elimination |
Tobias Winkler |
Current projects
Student | Type | Topic | Supervisor |
---|---|---|---|
Dario Veltri | Bachelor’s Thesis | Learning MDPs with SMT solving | Joshua Moerman |
Mengying Xue | Master’s Thesis | Efficient Analysis of Time-bounded Reachability in Markov Automata |
Tim Quatmann |
Denise Cassandra Fromme | Master’s Thesis | TBA | Lutz Klinkenberg |
Christina Gehnen | Bachelor’s Thesis | Automata-based Model Checking of Recursive Systems | 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 |
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 |
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
2020 | |
---|---|
[bibtex] [issue] | . Learning RFSA in Reverse, Bachelor Thesis, RWTH Aachen University, 2020. |
![]() ![]() |
. 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. |
![]() ![]() |
Linus Heck. Gradient descent on parametric Markov Chains, Bachelor Thesis, RWTH Aachen University, 31 Seiten, 2020. |
![]() ![]() |
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. |
2019 | |
![]() ![]() |
Ira Justus Fesefeldt. Proving termination of pointer programs on top of symbolic execution, Master Thesis, RWTH Aachen, 118 S., 2019. |
2011 | |
![]() |
Gustavo Quirós Araya. Static byte-code analysis for state space reduction, Master Thesis, RWTH Aachen University, 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. |
Show all |