BSc/MSc/Diplom Projects

If you are interested in writing your diplom/master/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	Talk to
March 2014	M	Control flow automaton based bounded model checking	Tim Lange
March 2014	B	Test case generation for a verification framework	Tim Lange
February 2014	B/M	Interprocedural Heap-Analysis using Contracts	Christina Jansen
January 2014	B	Schnelle Evaluierung probabilistisch primitiv rekursiver Funktionen	Benjamin Kaminski
June 2013	B/M	Solving Stochastic Games	Christian Dehnert
June 2013	B/M	Model Checking for Continuous-Time Markov Chains	Christian Dehnert
May 2013	M	A Conformance Relation for Symbolic Timed Automata with continuous Variables	Sabrina von Styp
Mar 2012	B/M/D	Observing Stochastic Games by Timed Automata	Christian Dehnert / Joost-Pieter Katoen
Mar 2012	D/M	Parametric LTL Model Checking of Markov Chains	Joost-Pieter Katoen
Mar 2012	D/M	Parametric Probabilistic Timed Automata	Joost-Pieter Katoen
May 2012	B	Dependency Analyses for Reconfigurable Component-Based Systems	Thomas Noll
Feb 2012	D/M	Verifying Randomised Algorithms using Layering	Joost-Pieter Katoen
June 2009	D/M	Probabilistic Model Checking with Interval Arithmetic	Joost-Pieter Katoen

Open since

Type

Topic

Talk to

March 2014

Control flow automaton based bounded model checking

Tim Lange

March 2014

Test case generation for a verification framework

Tim Lange

February 2014

B/M

Interprocedural Heap-Analysis using Contracts

Christina Jansen

January 2014

Schnelle Evaluierung probabilistisch primitiv rekursiver Funktionen

Benjamin Kaminski

June 2013

B/M

Solving Stochastic Games

Christian Dehnert

June 2013

B/M

Model Checking for Continuous-Time Markov Chains

Christian Dehnert

May 2013

A Conformance Relation for Symbolic Timed Automata with continuous Variables

Sabrina von Styp

Mar 2012

B/M/D

Observing Stochastic Games by Timed Automata

Christian Dehnert / Joost-Pieter Katoen

Mar 2012

D/M

Parametric LTL Model Checking of Markov Chains

Joost-Pieter Katoen

Mar 2012

D/M

Parametric Probabilistic Timed Automata

Joost-Pieter Katoen

May 2012

Dependency Analyses for Reconfigurable Component-Based Systems

Thomas Noll

Feb 2012

D/M

Verifying Randomised Algorithms using Layering

Joost-Pieter Katoen

June 2009

D/M

Probabilistic Model Checking with Interval Arithmetic

Joost-Pieter Katoen

D: Diplom project. M: Master project. B: Bachelor project.

Current Projects

Who	Type	Topic	Supervisor
Rim Jnidi	M	Modelling and Analysing Security Properties of a Multi-Level File System	Noll, van der Pol

Who

Type

Topic

Supervisor

Rim Jnidi

Modelling and Analysing Security Properties of a Multi-Level File System

Noll, van der Pol

D: Diplom project. M: Master project. B: Bachelor project.

Past Projects

2019
	Lukas Westhofen. Verifying Automotive C Code using Modern Software Model Checkers. at RWTH Aachen University, 2019.
2018
	Harold Bruintjes. Model-Based Reliability Analysis of Aerospace Systems, PhD defense at RWTH Aachen University, 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.
	Lea 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.
	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.
	Thomas Mertens. Efficient reuse of learnt information for control-flow oriented IC3 algorithms. Master thesis at RWTH Aachen University, 2016.
	Frederick Prinz. Generalisation methods for control-flow oriented IC3 algorithms. Master thesis at RWTH Aachen University, 2016.
	Tim 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.
	Hannah Arndt. Heap Abstraction Beyond Context-Freeness. Bachelor Thesis at RWTH Aachen University, 2016.
	Hanna 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
	Lukas Armborst. Generating Simulink Models from AADL system descriptions. Bachelor Thesis at RWTH Aachen University, 2015.
	Michael Beaumont. Efficient computation of weakest preconditions. Bachelor Thesis at RWTH Aachen University, 2015.
	Sascha Müller. Evaluating control-flow based inductive model checking algorithms. Master Thesis at RWTH Aachen University, 2015.
	Justin 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.
	Christoph Welzel. Thread-Modular Analysis of Heap-Manipulating Programs. Bachelor Thesis at RWTH Aachen University, 2015.
	Sascha Vincent Kurowski. Qualitative Model Checking of Markov Decision Processes on GPUs. Bachelor's Thesis at RWTH Aachen University, 2015.
	Sebastian Junges. Simplifying Dynamic Fault Trees by Graph Rewriting. Master Thesis at RWTH Aachen University, 2015.
	Xin Chen. Reachability Analysis of Non-Linear Hybrid Systems Using Taylor Models. Phd Thesis at RWTH Aachen University, 2015.
	Jens Katelaan. Modular Analysis of Concurrent Pointer Programs. Master's Thesis at RWTH Aachen University, 2015.
	Lukas Westhofen. On-the-fly Model Checking of Probabilistic Programs. Bachelor's Thesis at RWTH Aachen University, 2015.
2014
	Thomas Mertens. Optimization of Model Checking by Large Block Encoding. Bachelor Thesis at RWTH Aachen University, 2014.
	Lisa von Büttner. Probabilistic Backward Bisimulation on Interactive Markov Chains. Master Thesis at RWTH Aachen University, 2014.
	Frederick Prinz. Symbolic Model Checking of Probabilistic Systems using Multi-Terminal Binary Decision Diagrams. Bachelor Thesis at RWTH Aachen University, 2014.
	Philipp Florian. Efficiently Computing Poisson Probabilities for Model Checking Continuous-time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2014.
	Philipp Berger. GPU-aided Model Checking of Markov Decision Processes. Bachelor Thesis at RWTH Aachen University, 2014.
	Dimitri Bohlender. Accelerating Predicate Abstraction for Probabilistic Automata. Master Thesis at RWTH Aachen University, 2014.
	Tim Quatmann. Counterexamples for Expected Rewards on Discrete-time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2014.
	Christoph Matheja. Reconciling Decidability of Separation Logic Entailment and Graph Grammar Language Inclusion. Master Thesis at RWTH Aachen University, 2014.
	David 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.
	Christopher Kugler. A polytope library for the reachability analysis of hybrid systems. Master thesis at RWTH Aachen University, 2014.
	Dustin Hütter. SMT solving for linear integer arithmetic. Bachelor thesis at RWTH Aachen University, 2014.
	Maik Glatki. A zonotope library for hybrid systems reachability analysis. Bachelor thesis at RWTH Aachen University, 2014.
	Kai Driessen. Modular verification for PLC controlled hybrid systems. Master thesis at RWTH Aachen University, 2014.
2013
	Sergey 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.
	Benjamin Lucien Kaminski. Analyzing the Communication Behavior of LOOP+Omega Programs. Master Thesis at RWTH Aachen University, 2013.
	Gereon 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.
	Stefan 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.
	Henrik Schmitz. Parallel user-defined strategies for QFNRA. Diploma thesis at RWTH Aachen University, 2013.
	Thomas Osterland. Memory- and time-related action qualifiers in HSFCs. Bachelor thesis at RWTH Aachen University, 2013.
	Amith Belur Nagabushana. Minimal critical subsystems for PCTL. Master thesis at RWTH Aachen University, 2013.
	Georg Jenneßen. Solar tower optimisation with genetic algorithms. Diploma thesis at RWTH Aachen University, 2013.
	Kim Maren Haps. Datatypes and tools for the analysis of hybrid systems. Bachelor thesis at RWTH Aachen University, 2013.
	Matthias Ewert. Modellierung des Radialverdichters eines PKW-Abgasturboladers. Master thesis at RWTH Aachen University, 2013.
2012
	Hussein Hamid Baagil. Quantitative Message Sequence Graphs. Master Thesis at RWTH Aachen University, 2012.
	Florian 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.
	Max Görtz. Deciding MSO over Languages of Hypergraphs. Bachelorthesis at RWTH Aachen University, 2012.
	Alexander Dominik Weinert. Inferring Heap Abstraction Grammars. Bachelor Thesis at RWTH Aachen University, 2012.
	Tobias Hoffmann. Model Checking Quantifizierter Linearer Temporaler Logik über Pointerprogrammen. Diplomarbeit at RWTH Aachen University, 2012.
	Bernhard 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.
	Joachim Redies. An extension of the GiNaCRA library for the cylindrical algebraic decomposition. Bachelor thesis at RWTH Aachen Universtiy, 2012.
	Matthias Volk. Verification and synthesis for parametric Markov chains. Bachelor thesis at RWTH Aachen University, 2012.
	Sebastian 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.
	Kai Driessen. Counterexample-guided abstraction refinement for hybrid SFC verification. Bachelor thesis at RWTH Aachen University, 2012.
	Alin Ionascu. Modeling and controler synthesis of hybrid propulsion systems using artificial intelligence. Master thesis at RWTH Aachen University, 2012.
2011
	Henrik Barthels. Automata-Based Detection of Hypergraph Embeddings. Bachelorarbeit at RWTH Aachen University , 2011.
	Gereon Kremer. Syntaktische und semantische Analyse von Hyperkantenersetzungsgrammatiken zur Heapabstraktion. Bachelors Thesis at RWTH Aachen University, 2011.
	Markus Bals. Incremental Greibach Normal Form. Diploma Thesis at RWTH Aachen University, 2011.
	Christian Dehnert. Symbolic Bisimulation Minimization of Markov Models. Diplomarbeit at RWTH Aachen University, 2011.
	Lisa von Büttner. Stutter Simulation Minimisation. Bachelorarbeit at RWTH Aachen University, 2011.
	Florian Corzilius. Virtual Substitution in SMT Solving. Diploma thesis at RWTH Aachen, 2011.
	Hao Wu. Semantics and Analysis of Scenario-Aware Dataflow Specifications. Diploma Thesis at RWTH Aachen University, 2011.
	Hauke Schaper. Translation of Sequential Function Charts to Transition Systems. Bachelorarbeit at RWTH Aachen University, 2011.
	Silvio 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
	Friedrich 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.
	Falak Sher. Compositional Abstraction for Probabilistic Automata. Master Thesis at RWTH Aachen University, 2010.
	Maximilian 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.
	Christina 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.
	Stefan 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
	Sabrina von Styp. Towards a Testing Theory for Timed and Symbolic Systems. Diplomarbeit at RWTH Aachen University, 2009.
	Chitra 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.
	Pascal 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.
	Nils 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.
	Tim Kemna. Bisimulation Minimization in Probabilistic Model Checking. Master Thesis at University of Twente, 2007.
	Marcel Oldenkamp. Experimental Comparison of Probabilistic Model Checkers. Master Thesis at University of Twente, 2007.
2006
	Daniel Willems. Abstraktion zeitstetiger Markov-Ketten. Diploma Thesis at Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University, 2006.
	Gustavo Quirós. Static Byte-Code Analysis for State Space Reduction. Master Thesis at RWTH Aachen University, 2006.
2005
	Stefan 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.
	Jasper Berendsen. Reachability in Weighted Probabilistic Timed Automata. Master Thesis at University of Twente, 2005.

BSc/MSc/Diploma Topics
Teaching WS 2012/13
Hybrid Systems Group

We are looking for a HiWi for the Compiler Construction course. If you are interested, please contact Thomas Noll.

Joost-Pieter Katoen has been appointed as a member of the renowned Academia Europaea (Academy of Europe), a European, non-governmental association acting as an Academy whose members are scientists and scholars who collectively aim to promote learning, education and research.

Vacancies for postdoctoral researchers in "Automated Analysis of Probabilistic Programs". Application deadline: August 15, 2013.

Joost-Pieter Katoen has been awarded a Distinguished Professorship from the RWTH Aachen University.

The Hybrid Systems: Computation and Control (HSCC'13) conference in Philadelphia has been very successful: Hongfei Fu received the best student paper award for his paper "Approximating acceptance probabilities of CTMC-paths on multi-clock deterministic timed automata". Besides, the paper by Ilya Tkachev, Alexandru Mereacre, Alessandro Abate and Joost-Pieter Katoen was ranked second in the overall best paper award selection.

Joost-Pieter Katoen has been elected as Steering Committee Chair of ETAPS (www.etaps.org), the largest conference on theory and practice of software in Europe. He is the first non-UK ETAPS SC chair since the conference was initiated in 1998. More information here.

The Alumni-Magazine of RWTH Aachen University contains an interview with our former PhD student and postdoctoral researcher, Dr. Tingting Han.

HiWi's wanted to work in a new European Space Agency project for enhancing state-of-the-art design and analysis tools (COMPASS) for the next generation European rockets. Need programming and model checking affinity. See here for details and contact.

We offer openings for several PhD candidates in the area of
"Model-Based Design and Analysis for Dependable Software Systems". Deadline for application: September 14, 2012. For further information click here.

The Theory of Hybrid Systems Group offers two jobs as student assistants within the CEBug project. For more information, look here.

Dino Distefano received the prestigious Roger Needham Award for his work on software verification. This award is for a distinguished research contribution in computer science by a UK based researcher who has completed up to 10 years of post-doctoral research. Dr. Distefano was the first PhD student supervised by Joost-Pieter Katoen.

Marijn Jongerden received the German MMB (Messung, Modellierung und Bewertung von Rechensystemen) Award 2012 of the GI/ITG-Committee for Measurement, Modelling and Evaluation of Computing Systems for his PhD-thesis on "Model-based energy analysis of battery powered systems". His work was supervised by Boudewijn Haverkort (Twente) and Joost-Pieter Katoen.

Our paper "Formal Correctness, Safety, Dependability and Performance Analysis of a Satellite" has been accepted to ICSE 2012 in the track SE in Practice (18% acceptance rate). The paper treats a new satellite from the European Space Agency that was modeled and analyzed with modern tools during the actual satellite design.

Joost-Pieter Katoen will act as DJ in the "Nacht der Professoren" in the Apollo bar and cinema.