Thesis Projects

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 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
2019 July BSc / MSc Extending and applying weakest-preexpectation to parallel/concurrent probabilistic progams Ira Fesefeldt

Current projects

Student Type Topic Supervisor
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
DOI fulltext PDF [bibtex] Dan-Tuong Le. Quantitative Analysis of Counterexample Generation for Automata Learning, Bachelor Thesis, RWTH Aachen University, 2020.
restricted URL PDF [bibtex] Thomas Vogt. Learning RFSA in Reverse, Bachelor Thesis, RWTH Aachen University, 2020.
2011
fulltext PDF [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.
DownloadLinkFynn Mazurkiewicz. Parameter Synthesis for Continuous-Time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2020.
2019
DownloadLinkJan Š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.
DownloadLinkPaul 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.
DownloadLinkMirela 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.
DownloadLinkCaroline 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.
DownloadLinkLukas Westhofen. Verifying Automotive C Code using Modern Software Model Checkers. Master Thesis at RWTH Aachen University, 2019.
Show all