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
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
Laura Bamberger Bachelor’s Thesis Implementation of an LTL Model Checker for Probabilistic Push-Down Automata Tobias Winkler
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
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
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
Domenic Quirl Master’s Thesis FDE-Ready Parsing of Compile-Time Dynamic Languages Thomas Noll
Fabian Gasser Bachelor’s Thesis Analysis of Concurrent Probabilistic Programs with Shared Variables Thomas Noll

Award Winning Theses

Student Topic Award Supervisor
Christina Gehnen Automata-based Model Checking of Recursive Systems Preis der Fachgruppe Informatik der RWTH für eine herausragende Bachelorarbeit (2021) Tobias Winkler
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
DOI fulltext PDF [bibtex]
@masterthesis{LS2021,
title = {Learning probabilistic automata with SMT solving},
author = {Dario Veltri},
institution = {RWTH Aachen University},
pages = {71 Seiten},
type = {Bachelor Thesis},
year = {2021},
doi = {10.18154/RWTH-2021-03668},
url = { https://publications.rwth-aachen.de/record/817079},
}×
[issue] 		Dario Veltri. Learning probabilistic automata with SMT solving, Bachelor Thesis, RWTH Aachen University, 71 Seiten, 2021.
[bibtex]
@masterthesis{E2021,
title = {Efficient analysis of time-bounded reachability in markov automata},
author = {Mengying Xue},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/817764},
}×
[issue] 		Mengying Xue, Tim Quatmann. Efficient analysis of time-bounded reachability in markov automata, Master Thesis, RWTH Aachen University, 2021.
2020
[bibtex]
@masterthesis{LRR2020,
title = {Learning RFSA in Reverse},
author = {Thomas Vogt},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/792704},
}×
[issue] 		Thomas Vogt. Learning RFSA in Reverse, Bachelor Thesis, RWTH Aachen University, 2020.
DOI fulltext PDF [bibtex]
@masterthesis{QACGAL2020,
title = {Quantitative Analysis of Counterexample Generation for Automata Learning},
author = {Dan-Tuong Le},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-06326},
url = { https://publications.rwth-aachen.de/record/792705},
}×
[issue] 		Dan-Tuong Le. Quantitative Analysis of Counterexample Generation for Automata Learning, Bachelor Thesis, RWTH Aachen University, 2020.
[bibtex]
@masterthesis{PNEIAEDNNUSPWEB2020,
title = {Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds},
author = {Christopher Brix},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/802815},
}×
[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.
DOI fulltext PDF [bibtex]
@masterthesis{GMC2020,
title = {Gradient descent on parametric Markov Chains},
author = {Linus Heck},
institution = {RWTH Aachen University},
pages = {31 Seiten},
type = {Bachelor Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-10391},
url = { https://publications.rwth-aachen.de/record/804571},
}×
[issue] 		Linus Heck. Gradient descent on parametric Markov Chains, Bachelor Thesis, RWTH Aachen University, 31 Seiten, 2020.
DOI fulltext PDF [bibtex]
@masterthesis{IPGTAPP2020,
title = {Implementation of a Predicate-Guided Termination Analysis for Pointer Programs},
author = {Mohamed Khalifa},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-10469},
url = { https://publications.rwth-aachen.de/record/804692},
}×
[issue] 		Mohamed Khalifa. Implementation of a Predicate-Guided Termination Analysis for Pointer Programs, Bachelor Thesis, RWTH Aachen University, 2020.
[bibtex]
@masterthesis{RP2020,
title = {RPrIC3: PrIC3 for expected rewards},
author = {Adrian Gallus},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/805235},
}×
[issue] 		Adrian Gallus. RPrIC3: PrIC3 for expected rewards, Bachelor Thesis, RWTH Aachen University, 2020.
[bibtex]
@masterthesis{P2020,
title = {Parameter synthesis in probabilistic timed automata},
author = {Bram Kohlen},
institution = {RWTH Aachen University},
pages = {91 Seiten},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/811856},
}×
[issue] 		Bram Kohlen, Jip Josephine Spel. Parameter synthesis in probabilistic timed automata, Master Thesis, RWTH Aachen University, 91 Seiten, 2020.
DOI fulltext PDF [bibtex]
@masterthesis{D2020,
title = {Dynamic fault tree analysis using binary decision diagrams},
author = {Daniel Basgöze},
institution = {RWTH Aachen University},
pages = {76 Seiten},
type = {Bachelor Thesis},
year = {2020},
doi = {10.18154/RWTH-2021-03715},
url = { https://publications.rwth-aachen.de/record/817132},
}×
[issue] 		Daniel Basgöze, Matthias Volk, Shahid Khan. Dynamic fault tree analysis using binary decision diagrams, Bachelor Thesis, RWTH Aachen University, 76 Seiten, 2020.
[bibtex]
@masterthesis{A2020,
title = {A petri net semantics for boolean-logic driven markov processes},
author = {Lars Beckers},
institution = {RWTH Aachen University},
pages = {55 Seiten},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/818013},
}×
[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.
DownloadLinkFynn Mazurkiewicz. Parameter Synthesis for Continuous-Time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2020.
Show all