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 sinceTypeTopicSupervisor
2022 OctoberBScModelling and Verifying an Event-driven Language with Mean Times to HappenIra Fesefeldt
2022 OctoberMScQuantitative Entailments with Graph Grammars and Compatible PredicatesIra Fesefeldt
2020 OctoberMScProbabilistic Inference on Dynamic Bayesian Networks
Bahare Salmani
2020 FebruaryBSc/MScMetrics and Equivalences on formal Power Series for Probabilistic Program AnalysisLutz Klinkenberg
2020 FebruaryBSc/MScClosed-form Operations on Probability Generating Functions Lutz Klinkenberg

Award Winning Theses

StudentTopicAwardSupervisor
Marvin JansenDecidability and Complexity of Entailment Checking in Quantitative Separation LogicPreis der Fachgruppe Informatik der RWTH für eine herausragende Masterarbeit (2021)Kevin Batz
Christina GehnenAutomata-based Model Checking of Recursive SystemsPreis der Fachgruppe Informatik der RWTH für eine herausragende Bachelorarbeit (2021)Tobias Winkler
Jan SvejdaInterpretation-Based Violation Witness Validator. Master’s Thesis.DSA Industrial Award (2020)Jana Berger
Florian KeßlerOn 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 HiendlHuman-readable Scheduler Representation for Markov Decision Processes
Berthold Vöcking Master Award (2018)Tim Quatmann
Clara ScherbaumProbability Generating Function Semantics for Probabilistic Programs. Bachelor’s Thesis.itestra innovation Award (2016)
Benjamin Kaminski
Sebastian JungesSimplifying 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 SazonovProperty 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 KatelaanType Theory, Certified Programming and Compiler Verification. Bachelor’s Thesis.Schönebornpreis (2013)Thomas Noll
Falak SherCompositional Abstraction for Probabilistic Automata. Master’s Thesis.Microsoft Innovation Award (2010)Joost-Pieter Katoen

Current Projects (internal)

Past Projects

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.
[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.
DOI fulltext PDF [bibtex]
@masterthesis{T2022,
title = {Termination analysis of procedural pointer programs modelled by graph grammars},
author = {Mohamed Khalifa},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Diagramme},
type = {Master Thesis},
year = {2022},
doi = {10.18154/RWTH-2022-09096},
url = { https://publications.rwth-aachen.de/record/853842},
}×
[issue] 		Mohamed Khalifa. Termination analysis of procedural pointer programs modelled by graph grammars, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Diagramme, RWTH Aachen University, 2022.
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. Efficient analysis of time-bounded reachability in markov automata, Master 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.
[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{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{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.
Show all

Show all