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
Feb 2017 B How Fast is Your Modern Probabilistic Model Checker Sebastian Junges
Aug 2017 B/M Static state space reduction techniques for MDPs Sebastian Junges
Nov 2018 B Parameter synthesis for Continuous-Time Markov Chains Matthias Volk

Current projects

Student Type Topic Supervisor
Lutz Klinkenberg Master’s Thesis PGF Logics for Probabilistic Programs Benjamin Kaminski
Kevin Batz Master’s Thesis TBA Benjamin KaminskiSebastian JungesChristoph Matheja 
Sonja Skiba Bachelor’s Thesis Towards Complete Proof Rules for Almost-sure Termination of Probabilistic Programs Benjamin Kaminski
David Herzkamp Bachelor’s Thesis Hardness of Deciding Termination of Probabilistic Programs with Nondeterminism Benjamin Kaminski
Jan Svejda Master’s Thesis Formal Verification of Industrial C Code Philipp Berger
Hannah Arndt Master’s Thesis Randomized Meldable Heaps: A more formal proof of a less simple probabilistic data structure Christoph Matheja
Sally Chau Master’s Thesis TBA Christoph Matheja
Justus Fesefeldt Master’s Thesis TBA Christoph Matheja
Philipp Schroer Bachelor’s Thesis TBA Christoph Matheja
Bernhard Schulze Master’s Thesis TBA Christoph Matheja
Dustin Jungen Master’s Thesis SAT-Based Methods for Solving POMDP Problems Sebastian Junges
Sebastian Bartsch Bachelor’s Thesis Incremental Scanning (preliminary)
Thomas Noll
Caroline Jabs Bachelor’s Thesis Expected Run-Times of Probabilistic Pointer Programs (preliminary)
Thomas Noll
Mirela Mileva Bachelor’s Thesis Minimising Mealy Machines with Dependent Inputs (preliminary)
Thomas Noll

Award Winning Theses

Student Topic Award Supervisor
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 Modular Analysis of Concurrent Pointer Programs. 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

2019
DownloadLukas Westhofen. Verifying Automotive C Code using Modern Software Model Checkers. at RWTH Aachen University, 2019.
2018
Alexander Bork. Analysing Dynamic Fault Trees by GSPNs. Bachelor Thesis at RWTH Aachen University, 2018.
Sabrina Kowarsch. Modeling and Analysis of a Spacecraft Mission. Master Thesis at RWTH Aachen University, 2018.
Fabian Schneider. A Unified Algebraic Shape Domain. Master Thesis at RWTH Aachen University, 2018.
DownloadLea Hiendl. Human-readable Scheduler Representation for Markov Decision Processes. at RWTH Aachen University, 2018.
Felix Bier. From Forest Automata to Hyperedge Replacement Grammars and Back. Master Thesis at RWTH Aachen University, 2018.
2017
Sven Deserno. Probabilistic Model Checking for Markov Chain Families. Master Thesis at RWTH Aachen University, 2017.
Daniel Cloerkes. A Cyclic Proof System for Graph Grammar Inclusion. Bachelor Thesis at RWTH Aachen University, 2017.
Dustin Jungen. Repairs in Dynamic Fault Trees. Bachelor Thesis at RWTH Aachen University, 2017.
Michael Deutschen. Petri net semantics for Dynamic Fault Trees. Master Thesis at RWTH Aachen University, 2017.
DownloadKevin Batz. Proof Rules for Expected Run-Times of Probabilistic Programs. Bachelor Thesis at RWTH Aachen University, 2017.
2016
Ronja Nocon. Pattern based analysis of monotonicity on Dynamic Fault Trees. Bachelor Thesis at RWTH Aachen University, 2016.
DownloadThomas Mertens. Efficient reuse of learnt information for control-flow oriented IC3 algorithms. Master thesis at RWTH Aachen University, 2016.
DownloadFrederick Prinz. Generalisation methods for control-flow oriented IC3 algorithms. Master thesis at RWTH Aachen University, 2016.
DownloadTim Quatmann. Multi-Objective Model Checking of Markov Automata. Master Thesis at RWTH Aachen University, 2016.
Tom Janson. Accelerated Model Repair using Heuristic Analysis of Subsystems. Bachelor Thesis at RWTH Aachen University, 2016.
Isabelle Tülleners. Graph-based Heap Abstraction for Balanced Data Structures. Bachelor Thesis at RWTH Aachen University, 2016.
DownloadHannah Arndt. Heap Abstraction Beyond Context-Freeness. Bachelor Thesis at RWTH Aachen University, 2016.
DownloadHanna Franzen. Graph-Based Symbolic Execution for Pointer Programs with Data. Bachelor Thesis at RWTH Aachen University, 2016.
Simon Feiden. Extending Probability Generating Function Semantics to Negative Variable Valuations. at RWTH Aachen University, 2016.
Raoul Schaffranek. Modelling a Purely Functional Subset of EcmaScript2015. Bachelor Thesis at RWTH Aachen University, 2016.
Louis Wachtmeister. Analysing Cryptographically-Masked Information Flows Using Slicing. Bachelor Thesis at RWTH Aachen University, 2016.
David Korzeniewski. McMillan Prefixes for Stochastic Petri Nets. Master Thesis at RWTH Aachen University, 2016.
2015
DownloadLukas Armborst. Generating Simulink Models from AADL system descriptions. Bachelor Thesis at RWTH Aachen University, 2015.
DownloadMichael Beaumont. Efficient computation of weakest preconditions. Bachelor Thesis at RWTH Aachen University, 2015.
DownloadSascha Müller. Evaluating control-flow based inductive model checking algorithms. Master Thesis at RWTH Aachen University, 2015.
DownloadJustin Winkens. Loop Invariants in Probabilistic Programs. Bachelor Thesis at RWTH Aachen University, 2015.
Manuel Sascha Weiand. Checking Reachability Properties in Parametric MDPs. Master's Thesis at RWTH Aachen University, 2015.
Clara Scherbaum. Probability Generating Function Semantics for Probabilistic Programs. Bachelor Thesis at RWTH Aachen University, 2015.
LinkChristoph Welzel. Thread-Modular Analysis of Heap-Manipulating Programs. Bachelor Thesis at RWTH Aachen University, 2015.
DownloadSascha Vincent Kurowski. Qualitative Model Checking of Markov Decision Processes on GPUs. Bachelor's Thesis at RWTH Aachen University, 2015.
DownloadSebastian Junges. Simplifying Dynamic Fault Trees by Graph Rewriting. Master Thesis at RWTH Aachen University, 2015.
LinkJens Katelaan. Modular Analysis of Concurrent Pointer Programs. Master's Thesis at RWTH Aachen University, 2015.
DownloadLukas Westhofen. On-the-fly Model Checking of Probabilistic Programs. Bachelor's Thesis at RWTH Aachen University, 2015.
2014
DownloadThomas Mertens. Optimization of Model Checking by Large Block Encoding. Bachelor Thesis at RWTH Aachen University, 2014.
LinkLisa von Büttner. Probabilistic Backward Bisimulation on Interactive Markov Chains. Master Thesis at RWTH Aachen University, 2014.
DownloadFrederick Prinz. Symbolic Model Checking of Probabilistic Systems using Multi-Terminal Binary Decision Diagrams. Bachelor Thesis at RWTH Aachen University, 2014.
DownloadPhilipp Florian. Efficiently Computing Poisson Probabilities for Model Checking Continuous-time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2014.
DownloadPhilipp Berger. GPU-aided Model Checking of Markov Decision Processes. Bachelor Thesis at RWTH Aachen University, 2014.
DownloadDimitri Bohlender. Accelerating Predicate Abstraction for Probabilistic Automata. Master Thesis at RWTH Aachen University, 2014.
DownloadTim Quatmann. Counterexamples for Expected Rewards on Discrete-time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2014.
DownloadChristoph Matheja. Reconciling Decidability of Separation Logic Entailment and Graph Grammar Language Inclusion. Master Thesis at RWTH Aachen University, 2014.
DownloadDavid Korzeniewski. CEGAR for Computing High-Level Counterexamples for Probabilistic Systems. Bachelor Thesis at RWTH Aachen University, 2014.
Rim Jnidi. Modelling and Analysing Security Properties of a Multi-Level File System. Master Thesis at RWTH Aachen University, 2014.
LinkChristopher Kugler. A polytope library for the reachability analysis of hybrid systems. Master thesis at RWTH Aachen University, 2014.
LinkDustin Hütter. SMT solving for linear integer arithmetic. Bachelor thesis at RWTH Aachen University, 2014.
LinkMaik Glatki. A zonotope library for hybrid systems reachability analysis. Bachelor thesis at RWTH Aachen University, 2014.
LinkKai Driessen. Modular verification for PLC controlled hybrid systems. Master thesis at RWTH Aachen University, 2014.
2013
DownloadSergey Sazonov. Property Preservation under Bisimulations on Markov Automata. Master Thesis at RWTH Aachen University, 2013.
Yannis Samiro Discher. Graph-Based Interprocedural Analysis of Heap-Manipulating Programs. Bachelor Thesis at RWTH Aachen University, 2013.
DownloadBenjamin Lucien Kaminski. Analyzing the Communication Behavior of LOOP+Omega Programs. Master Thesis at RWTH Aachen University, 2013.
DownloadGereon Kremer. Isolating Real Roots Using Adaptable-Precision Interval Arithmetic. at RWTH Aachen University, 2013.
Tim Lange. Code-Based Model Minimization for PLC Code Verification. Master Thesis at RWTH Aachen University, 2013.
Christof Mroz. Formal Models for Diagnosability Analysis. Bachelor Thesis at RWTH Aachen University, 2013.
David Clermont. Analyzing the Timed Behavior of SLIM Specifications. Diplomarbeit at RWTH Aachen University, 2013.
DownloadStefan Schupp. Interval Constraint Propagation in SMT Compliant Decision Procedures. at RWTH Aachen University, 2013.
Andreas Vorpahl. Compositional counterexamples for MDPs. Master thesis at RWTH Aachen University, 2013.
Marian van de Veire. Minimal critical subsystems for probabilistic models with nondeterminism. Diploma thesis at RWTH Aachen University, 2013.
LinkHenrik Schmitz. Parallel user-defined strategies for QFNRA. Diploma thesis at RWTH Aachen University, 2013.
LinkThomas Osterland. Memory- and time-related action qualifiers in HSFCs. Bachelor thesis at RWTH Aachen University, 2013.
LinkAmith Belur Nagabushana. Minimal critical subsystems for PCTL. Master thesis at RWTH Aachen University, 2013.
LinkGeorg Jenneßen. Solar tower optimisation with genetic algorithms. Diploma thesis at RWTH Aachen University, 2013.
LinkKim Maren Haps. Datatypes and tools for the analysis of hybrid systems. Bachelor thesis at RWTH Aachen University, 2013.
LinkMatthias Ewert. Modellierung des Radialverdichters eines PKW-Abgasturboladers. Master thesis at RWTH Aachen University, 2013.
2012
DownloadHussein Hamid Baagil. Quantitative Message Sequence Graphs. Master Thesis at RWTH Aachen University, 2012.
DownloadFlorian Göbe. Transformation von Separation Logic Prädikaten durch Hyperkantenersetzungsgrammatiken. at RWTH Aachen, 2012.
Bart Postma. Modeling and Analysis of Dependable Space Systems. at University of Twente, 2012.
DownloadMax Görtz. Deciding MSO over Languages of Hypergraphs. Bachelorthesis at RWTH Aachen University, 2012.
DownloadAlexander Dominik Weinert. Inferring Heap Abstraction Grammars. Bachelor Thesis at RWTH Aachen University, 2012.
DownloadTobias Hoffmann. Model Checking Quantifizierter Linearer Temporaler Logik über Pointerprogrammen. Diplomarbeit at RWTH Aachen University, 2012.
DownloadBernhard Ern. Model-Based Criticality Analysis by Impact Isolation. at RWTH Aachen University, 2012.
Jens Katelaan. Type Theory, Certified Programming and Compiler Verification. Bachelor Thesis at RWTH Aachen University, 2012.
Sebastian Staack. Optimierung von Sensorkonfigurationen zur Fehlerdiagnose in technischen Systemen. Diplomarbeit at RWTH Aachen University, 2012.
Christoph Worreschk. Weighted Lumpability on Markov Chains. Bachelor Thesis at RWTH Aachen University, 2012.
Maik Scheffler. Hierarchical counterexamples for DTMCs – Case studies. Diploma thesis at RWTH Aachen University, 2012.
Canan Kasaci. Model-based resource monitoring and optimization. Master thesis at RWTH Aachen University, 2012.
LinkJoachim Redies. An extension of the GiNaCRA library for the cylindrical algebraic decomposition. Bachelor thesis at RWTH Aachen Universtiy, 2012.
LinkMatthias Volk. Verification and synthesis for parametric Markov chains. Bachelor thesis at RWTH Aachen University, 2012.
LinkSebastian Junges. On Gröbner bases in SMT-compliant decision procedures. Bachelor thesis at RWTH Aachen University, 2012.
Dennis Scully. Preprocessing for solving non-linear real-arithmetic formulas. Bachelor thesis at RWTH Aachen University, 2012.
LinkKai Driessen. Counterexample-guided abstraction refinement for hybrid SFC verification. Bachelor thesis at RWTH Aachen University, 2012.
LinkAlin Ionascu. Modeling and controler synthesis of hybrid propulsion systems using artificial intelligence. Master thesis at RWTH Aachen University, 2012.
2011
DownloadHenrik Barthels. Automata-Based Detection of Hypergraph Embeddings. Bachelorarbeit at RWTH Aachen University , 2011.
DownloadGereon Kremer. Syntaktische und semantische Analyse von Hyperkantenersetzungsgrammatiken zur Heapabstraktion. Bachelors Thesis at RWTH Aachen University, 2011.
DownloadMarkus Bals. Incremental Greibach Normal Form. Diploma Thesis at RWTH Aachen University, 2011.
DownloadChristian Dehnert. Symbolic Bisimulation Minimization of Markov Models. Diplomarbeit at RWTH Aachen University, 2011.
DownloadLisa von Büttner. Stutter Simulation Minimisation. Bachelorarbeit at RWTH Aachen University, 2011.
DownloadFlorian Corzilius. Virtual Substitution in SMT Solving. Diploma thesis at RWTH Aachen, 2011.
DownloadHao Wu. Semantics and Analysis of Scenario-Aware Dataflow Specifications. Diploma Thesis at RWTH Aachen University, 2011.
DownloadHauke Schaper. Translation of Sequential Function Charts to Transition Systems. Bachelorarbeit at RWTH Aachen University, 2011.
DownloadSilvio de Carolis. Zuverlässigkeitsanalyse dynamischer Fehlerbäume. at RWTH Aachen University, 2011.
Rafal Korzeniewski. Formal Approaches to System Diagnosability and Sensor Configuration Synthesis. at RWTH Aachen University, 2011.
2010
DownloadFriedrich Gretz. Invariant Generation for Linear Probabilistic Programs. Diplomarbeit at RWTH Aachen University, 2010.
Johanna Nellen. Konfluenzanalyse und Vervollständigung von Graphersetzungssystemen. Diplomarbeit at RWTH Aachen University, 2010.
Frank Fiedler. TripleT: Ein Werkzeug zum Echtzeittesten von reaktiven Systemen. Diplomarbeit at RWTH Aachen University, 2010.
Jan Scherer. An Eclipse-based Debugger for Embedded Systems Software. Diplomarbeit at RWTH Aachen University/University of Twente, 2010.
DownloadFalak Sher. Compositional Abstraction for Probabilistic Automata. Master Thesis at RWTH Aachen University, 2010.
LinkMaximilian R. Odenbrett. Explicit-State Model Checking of an Architectural Design Language using SPIN. Diplomarbeit at RWTH Aachen University, 2010.
Mark Bretsch. Automatic Code-Generation for a High-Level Virtual Platform from Process Network. Diplomarbeit at RWTH Aachen University, 2010.
DownloadChristina Jansen. Entwicklung eines Inferenzalgorithmus für Hyperkantenersetzungsgrammatiken. Diplomarbeit at RWTH Aachen University, 2010.
Dennis Guck. Analysis and scheduler synthesis of time-bounded reachability in continuous-time Markov decision processes. Bachelorarbeit at RWTH Aachen University, 2010.
DownloadStefan Herting. An Equivalence and Minimization Algorithm for CTMCs. Diplomarbeit at RWTH Aachen University, 2010.
Malte Kampschulte. Evaluation of radio models for the analysis of a gossiping MAC protocol. Bachelor Thesis at RWTH Aachen University, 2010.
2009
DownloadSabrina von Styp. Towards a Testing Theory for Timed and Symbolic Systems. Diplomarbeit at RWTH Aachen University, 2009.
DownloadChitra Hapsari Ayuningtyas. Probabilistic Message Sequence Charts. at RWTH Aachen University/University of Trento, 2009.
Ulrich Loup. Decision Problems over the Domain of the Real Numbers. Diploma thesis at RWTH Aachen, 2009.
Ralf Grossmann. Heapabstraktion durch partielle Graphreduktion mittels Graphgrammatiken . Diplomarbeit at Faculty of Mathematics, Computer Sciences and Natural Sciences,RWTH Aachen University , 2009.
Silvio de Carolis. Modeling and Analysis of Leader-Election Protocols in Ad-Hoc Networks . Bachelor Thesis at RWTH Aachen University, 2009.
LinkPascal Richter. Simulation und Auslegungsoptimierung solarthermischer Kraftwerke unter Einsatz evolutionärer Algorithmen und neuronaler Netze. Diploma thesis at RWTH Aachen University, 2009.
2008
Berteun Damman. Representing PCTL Counterexamples. Master Thesis at University of Twente, The Netherlands, 2008.
Mian Mohammad Junaid Tariq. An Agent-Based Simulation Environment for Large Scale Infrastructures of Heterogeneous Service-Based Devices. Master Thesis at RWTH Aachen University, 2008.
André Kolbe. Untersuchung der Anwendbarkeit des Timed Testing in der Eisenbahn-Signaltechnik. Diplomarbeit at RWTH Aachen University, 2008.
DownloadNils Jansen. Automaton-definable Tree Relations with Cardinality Constraints. Diploma Thesis at RWTH Aachen University, 2008.
2007
Lars Helge Haß. Gleichungsbasierte Abstraktionen für Rewrite Theories. Diplomarbeit at RWTH Aachen University, 2007.
Alexandru Mereacre. Modeling and Verification of Time-Inhomogeneous Markov Chains. Master Thesis at RWTH Aachen/University of Trento, 2007.
DownloadTim Kemna. Bisimulation Minimization in Probabilistic Model Checking. Master Thesis at University of Twente, 2007.
DownloadMarcel Oldenkamp. Experimental Comparison of Probabilistic Model Checkers. Master Thesis at University of Twente, 2007.
2006
DownloadDaniel Willems. Abstraktion zeitstetiger Markov-Ketten. Diploma Thesis at Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University, 2006.
DownloadGustavo Quirós. Static Byte-Code Analysis for State Space Reduction. Master Thesis at RWTH Aachen University, 2006.
2005
DownloadStefan Rieger. Analyse und Optimierung linearen Codes. Diploma Thesis at Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University, 2005.
Carsten Kern. MSCan - Ein Tool zur Analyse von Message Sequence Charts. Diploma Thesis at Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University, 2005.
Martin R. Neuhäußer. Abstraktion und Model Checking von Core Erlang-Programmen in Maude. Diplomarbeit at RWTH Aachen University, 2005.
DownloadJasper Berendsen. Reachability in Weighted Probabilistic Timed Automata. Master Thesis at University of Twente, 2005.