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]	Thomas Vogt. Learning RFSA in Reverse, Bachelor Thesis, RWTH Aachen University, 2020.
[bibtex] [issue]	Dan-Tuong Le. 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]	Adrian Gallus. 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
[bibtex] [issue]	Ira Justus Fesefeldt. Proving termination of pointer programs on top of symbolic execution, Master Thesis, RWTH Aachen, 118 S., 2019.
2011
[bibtex] [issue]	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