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 November BSc/MSc Probablistic Separation Logic for Concurrent Programs with Resources Ira Fesefeldt
2021 November BSc Modelling the Integers as List Graph Grammars to Analyse Termination Ira Fesefeldt
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 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

Award Winning Theses

Student Topic Award Supervisor
Marvin Jansen Decidability and Complexity of Entailment Checking in Quantitative Separation Logic Preis der Fachgruppe Informatik der RWTH für eine herausragende Masterarbeit (2021) Kevin Batz
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

Current Projects (internal)

Past Projects

2022
[bibtex]
@masterthesis{V2022,
title = {Verification of neural networks using binary tree search for branching},
author = {Lisa Pühl},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/847346},
}×
[issue] 		Lisa Pühl. Verification of neural networks using binary tree search for branching, Bachelor Thesis, RWTH Aachen University, 2022.
[bibtex]
@masterthesis{A2022,
title = {A unified slicing framework for probabilistic programs},
author = {Darion Haase},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/847345},
}×
[issue] 		Darion Haase. A unified slicing framework for probabilistic programs, Master Thesis, RWTH Aachen University, 2022.
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. Efficient analysis of time-bounded reachability in markov automata, Master Thesis, RWTH Aachen University, 2021.
[bibtex]
@masterthesis{A2021,
title = {Analysis of concurrent probabilistic programs with shared variables},
author = {Fabian Gasser},
institution = {RWTH Aachen University},
pages = {27 Seiten},
type = {Bachelor Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/840952},
}×
[issue] 		Fabian Gasser. Analysis of concurrent probabilistic programs with shared variables, Bachelor Thesis, RWTH Aachen University, 27 Seiten, 2021.
[bibtex]
@masterthesis{D2021,
title = {Decidability and complexity of entailment checking in quantitative separation logic},
author = {Marvin Jansen},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/829336},
}×
[issue] 		Marvin Jansen. Decidability and complexity of entailment checking in quantitative separation logic, Master Thesis, RWTH Aachen University, 2021.
[bibtex]
@masterthesis{W2021,
title = {Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs},
author = {Patrick Arens},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/829335},
}×
[issue] 		Patrick Arens. Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs, Bachelor Thesis, RWTH Aachen University, 2021.
[bibtex]
@masterthesis{IR2021,
title = {IDE-Ready parsing of compile-time dynamic languages},
author = {Domenic Quirl},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/826214},
}×
[issue] 		Domenic Quirl. IDE-Ready parsing of compile-time dynamic languages, Master Thesis, RWTH Aachen University, 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.
Show all

Show all