Thesis Projects

If you are interested in writing your BSc or MSc thesis in the MOVES group, please contact Prof. Dr. Joost-Pieter Katoen, Prof. Dr. Thomas Noll, or send a general request to thesis at i2.informatik.rwth-aachen.de (kindly include your transcript of records).

Award Winning Theses

StudentTopicAwardSupervisor
Tom BiskupInvariant-based Strategy Synthesis for Nondeterministic Probabilistic ProgramsBerthold Vöcking Master Award (2023)Kevin Batz
Tobias Winkler
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

Past Projects

2024
DOI fulltext PDF [bibtex]
@masterthesis{CTA2024,
title = {Combining integer programs and graph grammars: Theory and implementation in Attestor},
author = {Alexander Ferber},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-00784},
url = { https://publications.rwth-aachen.de/record/977552},
}×
[issue] 		Alexander Ferber. Combining integer programs and graph grammars: Theory and implementation in Attestor, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{C2024,
title = {Complexity and decidability of multi-objective stochastic games},
author = {Tobias Winkler},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02592},
url = { https://publications.rwth-aachen.de/record/980848},
}×
[issue] 		Tobias Winkler. Complexity and decidability of multi-objective stochastic games, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{I2024,
title = {Invariant-based strategy synthesis for nondeterministic probabilistic programs},
author = {Tom Biskup},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02594},
url = { https://publications.rwth-aachen.de/record/980850},
}×
[issue] 		Tom Biskup. Invariant-based strategy synthesis for nondeterministic probabilistic programs, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{C2024,
title = {Compositional control-flow reduction for probabilistic model checking},
author = {Naomi Barth},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02596},
url = { https://publications.rwth-aachen.de/record/980852},
}×
[issue] 		Naomi Barth. Compositional control-flow reduction for probabilistic model checking, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{PS2024,
title = {Proving termination of probabilistic recursive programs via SMT-solving},
author = {Leo Mommers},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02602},
url = { https://publications.rwth-aachen.de/record/980858},
}×
[issue] 		Leo Mommers. Proving termination of probabilistic recursive programs via SMT-solving, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{P2024,
title = {Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning},
author = {Johannes Lehmann},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02603},
url = { https://publications.rwth-aachen.de/record/980859},
}×
[issue] 		Johannes Lehmann. Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning, Master Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{ARLGR2024,
title = {Application of Reinforcement Learning to the Game of Reversi++},
author = {Songran Shi},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-04092},
url = { https://publications.rwth-aachen.de/record/984514},
}×
[issue] 		Songran Shi. Application of Reinforcement Learning to the Game of Reversi++, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{M2024,
title = {Model checking pPDA vs unambiguous automata},
author = {Anastasiia Petrova},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-06745},
url = { https://publications.rwth-aachen.de/record/989355},
}×
[issue] 		Anastasiia Petrova. Model checking pPDA vs unambiguous automata, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{MBN2024,
title = {Most probable explanations in Bayesian Networks via weighted programming},
author = {Dinis Vitorino},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-06746},
url = { https://publications.rwth-aachen.de/record/989356},
}×
[issue] 		Dinis Vitorino. Most probable explanations in Bayesian Networks via weighted programming, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{SJ2024,
title = {Semantics-preserving transformation of Java source code},
author = {Frederik Heigold},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/991802},
}×
[issue] 		Frederik Heigold. Semantics-preserving transformation of Java source code, Bachelor Thesis, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{O2024,
title = {Optimized routing for shuttling-based quantum processing architectures},
author = {Roy Hermanns},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/991804},
}×
[issue] 		Roy Hermanns. Optimized routing for shuttling-based quantum processing architectures, Master Thesis, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{H2024,
title = {Heuristic synthesis of spare parts inventories using dynamic fault trees},
author = {Jakob van Sprang},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/991805},
}×
[issue] 		Jakob van Sprang. Heuristic synthesis of spare parts inventories using dynamic fault trees, Bachelor Thesis, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{IGHPS2024,
title = {Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm},
author = {Sven Büge},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/992674},
}×
[issue] 		Sven Büge. Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm, Bachelor Thesis, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{E2024,
title = {Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs},
author = {Patrick Nossol},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-09539},
url = { https://publications.rwth-aachen.de/record/994779},
}×
[issue] 		Patrick Nossol. Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs, Master Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{D2024,
title = {Distributional invariants for probabilistic programs},
author = {Daniel Zilken},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/995438},
}×
[issue] 		Daniel Zilken. Distributional invariants for probabilistic programs, Master Thesis, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{A2024,
title = {A deductive verifier for probabilistic programs},
author = {Philipp Schroer},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-11340},
url = { https://publications.rwth-aachen.de/record/998370},
}×
[issue] 		Philipp Schroer. A deductive verifier for probabilistic programs, Master Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
2023
[bibtex]
@masterthesis{C2023,
title = {Comparison of symbolic maximal end component decomposition algorithms},
author = {Felix Faber},
institution = {RWTH Aachen University},
pages = {61 Seiten : Illustrationen, Diagramme},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/974509},
}×
[issue] 		Felix Faber. Comparison of symbolic maximal end component decomposition algorithms, Bachelor Thesis, RWTH Aachen University, 61 Seiten : Illustrationen, Diagramme, 2023.
[bibtex]
@masterthesis{SM2023,
title = {Strategy computation for a Markovian disease spread model},
author = {Gergana Tropcheva},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977478},
}×
[issue] 		Gergana Tropcheva. Strategy computation for a Markovian disease spread model, Bachelor Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{A2023,
title = {Automatic algorithm selection for probabilistic model checking using machine learning},
author = {Umut Yigit Dural},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977479},
}×
[issue] 		Umut Yigit Dural. Automatic algorithm selection for probabilistic model checking using machine learning, Bachelor Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{RM2023,
title = {Representing Markov models by extending the intermediate model checking language},
author = {Jialei Yao},
institution = {RWTH Aachen University},
pages = {67 Seiten : Illustrationen},
type = {Master Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977529},
}×
[issue] 		Jialei Yao. Representing Markov models by extending the intermediate model checking language, Master Thesis, RWTH Aachen University, 67 Seiten : Illustrationen, 2023.
[bibtex]
@masterthesis{A2023,
title = {Approximate probabilistic bisimulations and quotienting},
author = {Timm Spork},
institution = {RWTH Aachen University},
pages = {186 Seiten : Illustrationen},
type = {Master Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977530},
}×
[issue] 		Timm Spork. Approximate probabilistic bisimulations and quotienting, Master Thesis, RWTH Aachen University, 186 Seiten : Illustrationen, 2023.
[bibtex]
@masterthesis{SC2023,
title = {Slicing COBOL software for program understanding},
author = {Stefan Busch},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977551},
}×
[issue] 		Stefan Busch. Slicing COBOL software for program understanding, Bachelor Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{A2023,
title = {Architecture-oriented safety verification of transformer networks via program analysis},
author = {Daniel Alexander Heinen},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977553},
}×
[issue] 		Daniel Alexander Heinen. Architecture-oriented safety verification of transformer networks via program analysis, Master Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{A2023,
title = {Automated assessment of regular expressions},
author = {Ebru Kusak},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977555},
}×
[issue] 		Ebru Kusak. Automated assessment of regular expressions, Bachelor Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{E2023,
title = {Evaluation of out-of-distribution detection techniques for dataset filtering},
author = {Lasse van der Woude},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977559},
}×
[issue] 		Lasse van der Woude. Evaluation of out-of-distribution detection techniques for dataset filtering, Master Thesis, RWTH Aachen University, 2023.
Show all