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
Student | Topic | Award | Supervisor |
---|---|---|---|
Tom Biskup | Invariant-based Strategy Synthesis for Nondeterministic Probabilistic Programs | Berthold Vöcking Master Award (2023) | Kevin Batz Tobias Winkler |
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) | Jana 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
2024 | |
---|---|
[bibtex] [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. |
[bibtex] [issue] | Tobias Winkler. Complexity and decidability of multi-objective stochastic games, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024. |
[bibtex] [issue] | Tom Biskup. Invariant-based strategy synthesis for nondeterministic probabilistic programs, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024. |
[bibtex] [issue] | Naomi Barth. Compositional control-flow reduction for probabilistic model checking, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024. |
[bibtex] [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. |
[bibtex] [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. |
[bibtex] [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. |
[bibtex] [issue] | Anastasiia Petrova. Model checking pPDA vs unambiguous automata, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024. |
[bibtex] [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] [issue] | Frederik Heigold. Semantics-preserving transformation of Java source code, Bachelor Thesis, RWTH Aachen University, 2024. |
[bibtex] [issue] | Roy Hermanns. Optimized routing for shuttling-based quantum processing architectures, Master Thesis, RWTH Aachen University, 2024. |
[bibtex] [issue] | Jakob van Sprang. Heuristic synthesis of spare parts inventories using dynamic fault trees, Bachelor Thesis, RWTH Aachen University, 2024. |
[bibtex] [issue] | Sven Büge. Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm, Bachelor Thesis, RWTH Aachen University, 2024. |
[bibtex] [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] [issue] | Daniel Zilken. Distributional invariants for probabilistic programs, Master Thesis, RWTH Aachen University, 2024. |
2023 | |
[bibtex] [issue] | Felix Faber. Comparison of symbolic maximal end component decomposition algorithms, Bachelor Thesis, RWTH Aachen University, 61 Seiten : Illustrationen, Diagramme, 2023. |
[bibtex] [issue] | Gergana Tropcheva. Strategy computation for a Markovian disease spread model, Bachelor Thesis, RWTH Aachen University, 2023. |
[bibtex] [issue] | Umut Yigit Dural. Automatic algorithm selection for probabilistic model checking using machine learning, Bachelor Thesis, RWTH Aachen University, 2023. |
[bibtex] [issue] | Jialei Yao. Representing Markov models by extending the intermediate model checking language, Master Thesis, RWTH Aachen University, 67 Seiten : Illustrationen, 2023. |
[bibtex] [issue] | Timm Spork. Approximate probabilistic bisimulations and quotienting, Master Thesis, RWTH Aachen University, 186 Seiten : Illustrationen, 2023. |
[bibtex] [issue] | Stefan Busch. Slicing COBOL software for program understanding, Bachelor Thesis, RWTH Aachen University, 2023. |
[bibtex] [issue] | Daniel Alexander Heinen. Architecture-oriented safety verification of transformer networks via program analysis, Master Thesis, RWTH Aachen University, 2023. |
[bibtex] [issue] | Ebru Kusak. Automated assessment of regular expressions, Bachelor Thesis, RWTH Aachen University, 2023. |
[bibtex] [issue] | Lasse van der Woude. Evaluation of out-of-distribution detection techniques for dataset filtering, Master Thesis, RWTH Aachen University, 2023. |
2022 | |
[bibtex] [issue] | Darion Haase. A unified slicing framework for probabilistic programs, Master Thesis, RWTH Aachen University, 2022. |
[bibtex] [issue] | Lisa Pühl. Verification of neural networks using binary tree search for branching, Bachelor Thesis, RWTH Aachen University, 2022. |
[bibtex] [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. |
[bibtex] [issue] | Jan Jeremy Tugsbayar. Verification of leader election protocols for dynamic networks, Bachelor Thesis, RWTH Aachen University, 2022. |
[bibtex] [issue] | Dominic Sebastian Meiser. Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation, Bachelor Thesis, RWTH Aachen University, 2022. |
[bibtex] [issue] | Denis Kuksaus. Markow-Entscheidungsprozesse mit mehreren Agenten: Ein Überblick mit Fokus auf effiziente Aufgabenverteilung, Master Thesis, RWTH Aachen University, 2022. |
[bibtex] [issue] | Jan Erik Karuc. Verifying parametric Markov models using decision diagrams, Bachelor Thesis, RWTH Aachen University, 2022. |
[bibtex] [issue] | Christina Gehnen. POMDP-based execution models for probabilistic programs with partial observability, Master Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2022. |
[bibtex] [issue] | Jonas Seidel. Comparison of heuristics for branching in neural network verification, Bachelor Thesis, RWTH Aachen University, 75 Seiten : Illustrationen, 2022. |
[bibtex] [issue] | Caroline Jabs. Novelty-detection-based split selection heuristics for neural network verification, Master Thesis, RWTH Aachen University, 2022. |
[bibtex] [issue] | Ben Sturgis. Automatic verification of loop invariants in weighted programs, Bachelor Thesis, RWTH Aachen University, 2022. |
[bibtex] [issue] | Christian Blumenthal. Inference in discrete probabilistic programs using probability generating functions, Master Thesis, RWTH Aachen University, 2022. |
[bibtex] [issue] | Laura Bamberger. Implementation of an LTL model checker for probabilistic pushdown automata, Bachelor Thesis, RWTH Aachen University, 2022. |
2021 | |
[bibtex] [issue] | Dario Veltri. Learning probabilistic automata with SMT solving, Bachelor Thesis, RWTH Aachen University, 71 Seiten, RWTH Aachen University, 2021. |
[bibtex] [issue] | Mengying Xue. Efficient analysis of time-bounded reachability in markov automata, Master Thesis, RWTH Aachen University, 2021. |
[bibtex] [issue] | Domenic Quirl. IDE-Ready parsing of compile-time dynamic languages, Master Thesis, RWTH Aachen University, 2021. |
[bibtex] [issue] | Patrick Arens. Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs, Bachelor Thesis, RWTH Aachen University, 2021. |
[bibtex] [issue] | Marvin Jansen. Decidability and complexity of entailment checking in quantitative separation logic, Master Thesis, RWTH Aachen University, 2021. |
[bibtex] [issue] | Fabian Gasser. Analysis of concurrent probabilistic programs with shared variables, Bachelor Thesis, RWTH Aachen University, 27 Seiten, 2021. |
[bibtex] [issue] | Alexander Nikolai Bork. Underapproximations for indefinite-horizon POMDPS, Master Thesis, RWTH Aachen University, 2021. |
[bibtex] [issue] | Christina Gehnen. Automata-based model checking of recursive systems, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2021. |
2020 | |
[bibtex] [issue] | . Learning RFSA in Reverse, Bachelor Thesis, RWTH Aachen University, 2020. |
[bibtex] [issue] | . Quantitative Analysis of Counterexample Generation for Automata Learning, Bachelor Thesis, RWTH Aachen University, 2020. |
[bibtex] [issue] | Alexander Hoppen. Design and implementation of an interactive exploration tool for probabilistic programs, Master Thesis, RWTH Aachen University, 124 Seiten, 2020. |
[bibtex] [issue] | . Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds, Master Thesis, RWTH Aachen University, 2020. |
[bibtex] [issue] | Linus Heck. Gradient descent on parametric Markov Chains, Bachelor Thesis, RWTH Aachen University, 31 Seiten, 2020. |
[bibtex] [issue] | Mohamed Khalifa. Implementation of a Predicate-Guided Termination Analysis for Pointer Programs, Bachelor Thesis, RWTH Aachen University, 2020. |
[bibtex] [issue] | . RPrIC3: PrIC3 for expected rewards, Bachelor Thesis, RWTH Aachen University, 2020. |
[bibtex] [issue] | Bram Kohlen. Parameter synthesis in probabilistic timed automata, Master Thesis, RWTH Aachen University, 91 Seiten, 2020. |
[bibtex] [issue] | Daniel Basgöze. Dynamic fault tree analysis using binary decision diagrams, Bachelor Thesis, RWTH Aachen University, 76 Seiten, 2020. |
[bibtex] [issue] | Lars Beckers. A petri net semantics for boolean-logic driven markov processes, Master Thesis, RWTH Aachen University, 55 Seiten, 2020. |
[bibtex] [issue] | Robin Drahovsky. Parameter synthesis in bayesian networks, Master Thesis, RWTH Aachen University, 2020. |
2019 | |
[bibtex] [issue] | Ira Justus Fesefeldt. Proving termination of pointer programs on top of symbolic execution, Master Thesis, RWTH Aachen University, 118 S., 2019. |
2011 | |
[bibtex] [issue] | Gustavo Quirós Araya. Static byte-code analysis for state space reduction, Master Thesis, RWTH Aachen University, VIII, 101 S., Publikationsserver der RWTH Aachen University, 2011. |