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
Oct 2015 M Invariants for Conditional Weakest-Preexpectations Benjamin Kaminski
Feb 2017 B How Fast is Your Modern Probabilistic Model Checker Sebastian Junges
Apr 2017 B Parameter synthesis for Continuous-Time Markov Chains Matthias Volk
Aug 2017 B/M Static state space reduction techniques for MDPs Sebastian Junges
Sep 2017 B Topological strategy iteration for MDP model checking Tim Quatmann

Current projects

Student Type Topic Supervisor
Lukas Westhofen Master Thesis Formal Verification of Industrial C Code Philipp Berger

Past projects

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.
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.
Kevin 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.