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@i2.informatik.rwth-aachen.de (kindly include your transcript of records and indicate when you would like to start working on your project).

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

2026

Bachelor’s thesis
Belief-tracking policies for partially observable MDPs via randomized finite-state controllers
Ole Dannemeyer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tim Quatmann
Consultants: Tobias Winkler, Lisa Pühl
RWTH record for Belief-tracking policies for partially observable MDPs via randomized finite-state controllers BibTeX for Belief-tracking policies for partially observable MDPs via randomized finite-state controllers
Bachelor’s thesis
Distribution transformers for probabilistic programs: a study of inductive definability
Felix Euting
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
RWTH record for Distribution transformers for probabilistic programs: a study of inductive definability BibTeX for Distribution transformers for probabilistic programs: a study of inductive definability
Bachelor’s thesis
Semantic equivalences of probabilistic programs and their underlying Markov chains
Philip Strüwer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tim Quatmann
Consultants: Daniel Johannes Zilken, Jan-Gustav Michnia
RWTH record for Semantic equivalences of probabilistic programs and their underlying Markov chains BibTeX for Semantic equivalences of probabilistic programs and their underlying Markov chains
Master’s thesis
Bounds for quantum weakest preconditions
Jonas Deutsch
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Dominique Unruh
Consultants: Christina Gehnen
PDF of Bounds for quantum weakest preconditions RWTH record for Bounds for quantum weakest preconditions BibTeX for Bounds for quantum weakest preconditions
Bachelor’s thesis
Visualizing execution-schedules for conveyor-based quantum computing hardware
Xufei Xie
RWTH Aachen University
Advisers: Thomas Noll, Hendrik Bluhm
Consultants: Roy Hermanns
RWTH record for Visualizing execution-schedules for conveyor-based quantum computing hardware BibTeX for Visualizing execution-schedules for conveyor-based quantum computing hardware
Master’s thesis
Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning
Jonas Seidel
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
PDF of Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning RWTH record for Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning BibTeX for Sound and complete proof rules for almost-sure termination: from probabilistic control-flow graphs to program-level reasoning
Bachelor’s thesis
Which probabalistic programs are modelcheckable?
Samuel Akinlaja
Rheinisch-Westfälische Technische Hochschule Aachen
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
RWTH record for Which probabalistic programs are modelcheckable?BibTeX for Which probabalistic programs are modelcheckable?
Bachelor’s thesis
Heuristic circuit mapping strategies for the SpinBus architecture
Martin Baum
RWTH Aachen University
Advisers: Thomas Noll, Hendrik Bluhm
PDF of Heuristic circuit mapping strategies for the SpinBus architecture RWTH record for Heuristic circuit mapping strategies for the SpinBus architecture BibTeX for Heuristic circuit mapping strategies for the SpinBus architecture

2025

PhD thesis
Deductive reasoning about concurrent probabilistic programs
Ira Justus Fesefeldt
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Lars Birkedal
PDF of Deductive reasoning about concurrent probabilistic programs RWTH record for Deductive reasoning about concurrent probabilistic programs BibTeX for Deductive reasoning about concurrent probabilistic programs
Master’s thesis
Multi‐agent path finding for reversible conveyors
Dominic Sebastian Meiser
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Roy Hermanns
PDF of Multi‐agent path finding for reversible conveyors RWTH record for Multi‐agent path finding for reversible conveyors BibTeX for Multi‐agent path finding for reversible conveyors
Bachelor’s thesis
Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies
Muhammad Asad Murtaza Butt
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Hannah Mertens
RWTH record for Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies BibTeX for Extending the assume–guarantee framework for parametric probabilistic automata : From robust valuations to the limits of robust strategies
Master’s thesis
Compilation of quantum programs with control flow primitives in superposition
Sascha Thiemann
RWTH Aachen University
Advisers: Thomas Noll, Dominique Unruh
RWTH record for Compilation of quantum programs with control flow primitives in superposition BibTeX for Compilation of quantum programs with control flow primitives in superposition
Master’s thesis
Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates
Rico Stanosek
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates BibTeX for Cost-reliability optimal spare part allocation in dynamic fault trees with relaxed spare gates
Bachelor’s thesis
Scalable qubit routing on the conveyor-based SpinBus architecture
Dobromir Panayotov
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Roy Hermanns
RWTH record for Scalable qubit routing on the conveyor-based SpinBus architecture BibTeX for Scalable qubit routing on the conveyor-based SpinBus architecture
Bachelor’s thesis
Evaluating tool support for fault tree analysis of satellite constellations
Mareike Metzler
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
PDF of Evaluating tool support for fault tree analysis of satellite constellations RWTH record for Evaluating tool support for fault tree analysis of satellite constellations BibTeX for Evaluating tool support for fault tree analysis of satellite constellations
Bachelor’s thesis
Implementation of PRNG-based elimination of intermediate measurements in quantum circuits
Sophia Greiwe
RWTH Aachen University
Advisers: Thomas Noll, Dominique Unruh
RWTH record for Implementation of PRNG-based elimination of intermediate measurements in quantum circuits BibTeX for Implementation of PRNG-based elimination of intermediate measurements in quantum circuits
Bachelor’s thesis
Exploration of certificate sharing for neural network verification
Glen Jordan Grant
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix, Xaver Fink
RWTH record for Exploration of certificate sharing for neural network verification BibTeX for Exploration of certificate sharing for neural network verification
Bachelor’s thesis
Quantum circuit optimization through eliminating and deferring mid-circuit measurements
Johannes Peter Valentin Gaidetzka
RWTH Aachen University
Advisers: Thomas Noll, Dominique Unruh
RWTH record for Quantum circuit optimization through eliminating and deferring mid-circuit measurements BibTeX for Quantum circuit optimization through eliminating and deferring mid-circuit measurements
Bachelor’s thesis
On the relation of rely-guarantee and assume-guarantee reasoning
Marcel Eissing
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Lena Verscht, Hannah Mertens
PDF of On the relation of rely-guarantee and assume-guarantee reasoning RWTH record for On the relation of rely-guarantee and assume-guarantee reasoning BibTeX for On the relation of rely-guarantee and assume-guarantee reasoning
Bachelor’s thesis
Modeling non-deterministic quantum programs for model checking
Kaleb Kierner
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Dominique Unruh
Consultants: Christina Gehnen
PDF of Modeling non-deterministic quantum programs for model checking RWTH record for Modeling non-deterministic quantum programs for model checking BibTeX for Modeling non-deterministic quantum programs for model checking
Bachelor’s thesis
Implementing the denotational semantics of probabilistic programs
Elbeck Lazaridi
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Daniel Johannes Zilken
RWTH record for Implementing the denotational semantics of probabilistic programs BibTeX for Implementing the denotational semantics of probabilistic programs
PhD thesis
Analysis of probabilistic programs using generating functions
Lutz Klinkenberg
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Laura Kovacs
PDF of Analysis of probabilistic programs using generating functions RWTH record for Analysis of probabilistic programs using generating functions BibTeX for Analysis of probabilistic programs using generating functions
Master’s thesis
Effective quantifier-based reasoning for quantitative deductive verification
Emil Beothy-Elo
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Philipp Schroer, Darion Haase
PDF of Effective quantifier-based reasoning for quantitative deductive verification RWTH record for Effective quantifier-based reasoning for quantitative deductive verification BibTeX for Effective quantifier-based reasoning for quantitative deductive verification
Master’s thesis
Automata-based semantics for the probabilistic programming language ReDiP
Dominik Geißler
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Automata-based semantics for the probabilistic programming language ReDiP RWTH record for Automata-based semantics for the probabilistic programming language ReDiP BibTeX for Automata-based semantics for the probabilistic programming language ReDiP

2024

Master’s thesis
MARVEL: A stepwise debugging tool for Markov models in the PRISM-language
Patrick Arens
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
RWTH record for MARVEL: A stepwise debugging tool for Markov models in the PRISM-language BibTeX for MARVEL: A stepwise debugging tool for Markov models in the PRISM-language
Bachelor’s thesis
Testing the applicability of robustness evaluation methods for neural networks on nonlinear real arithmetic problems using α-β-CROWN and foolbox
Julia Walczak
RWTH Aachen University
Advisers: Thomas Noll, Erika Abraham
Consultants: Christopher Jan-Steffen Brix
RWTH record for Testing the applicability of robustness evaluation methods for neural networks on nonlinear real arithmetic problems using α-β-CROWN and foolbox BibTeX for Testing the applicability of robustness evaluation methods for neural networks on nonlinear real arithmetic problems using α-β-CROWN and foolbox
Bachelor’s thesis
Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks
Yejun Tang
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks BibTeX for Transfer of branching heuristics for neural network verification to alpha-beta-CROWN and evaluation of large-scale verification benchmarks
PhD thesis
Automated deductive verification of probabilistic programs
Kevin Batz
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Ichiro Hasuo
PDF of Automated deductive verification of probabilistic programs RWTH record for Automated deductive verification of probabilistic programs BibTeX for Automated deductive verification of probabilistic programs
PhD thesis
Probabilistic model checking and parameter tuning for Bayesian networks
Bahare Salmani Barzoki
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Luc de Raedt
PDF of Probabilistic model checking and parameter tuning for Bayesian networks RWTH record for Probabilistic model checking and parameter tuning for Bayesian networks BibTeX for Probabilistic model checking and parameter tuning for Bayesian networks
Master’s thesis
A deductive verifier for probabilistic programs
Philipp Schroer
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Peter Müller
Consultants: Kevin Batz, Benjamin Kaminski, Christoph Matheja
PDF of A deductive verifier for probabilistic programs RWTH record for A deductive verifier for probabilistic programs BibTeX for A deductive verifier for probabilistic programs
PhD thesis
Applying software model checking: experiences and advancements
Philipp Berger
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Dirk Beyer
PDF of Applying software model checking: experiences and advancements RWTH record for Applying software model checking: experiences and advancements BibTeX for Applying software model checking: experiences and advancements
Master’s thesis
Distributional invariants for probabilistic programs
Daniel Johannes Zilken
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Kevin Batz, Tobias Winkler
RWTH record for Distributional invariants for probabilistic programs BibTeX for Distributional invariants for probabilistic programs
Master’s thesis
Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs
Patrick Nossol
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen, Ira Justus Fesefeldt
PDF of Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs RWTH record for Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs BibTeX for Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs
Bachelor’s thesis
Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm
Sven Büge
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Alexander Nikolai Bork
RWTH record for Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm BibTeX for Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm
Bachelor’s thesis
Heuristic synthesis of spare parts inventories using dynamic fault trees
Jakob van Sprang
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Heuristic synthesis of spare parts inventories using dynamic fault trees BibTeX for Heuristic synthesis of spare parts inventories using dynamic fault trees
Master’s thesis
Optimized routing for shuttling-based quantum processing architectures
Roy Hermanns
RWTH Aachen University
Advisers: Thomas Noll, Hendrik Bluhm
RWTH record for Optimized routing for shuttling-based quantum processing architectures BibTeX for Optimized routing for shuttling-based quantum processing architectures
Bachelor’s thesis
Semantics-preserving transformation of Java source code
Frederik Heigold
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Semantics-preserving transformation of Java source code BibTeX for Semantics-preserving transformation of Java source code
Bachelor’s thesis
Most probable explanations in Bayesian Networks via weighted programming
Dinis Vitorino
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler, Kevin Batz
PDF of Most probable explanations in Bayesian Networks via weighted programming RWTH record for Most probable explanations in Bayesian Networks via weighted programming BibTeX for Most probable explanations in Bayesian Networks via weighted programming
Bachelor’s thesis
Model checking pPDA vs unambiguous automata
Anastasiia Petrova
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Model checking pPDA vs unambiguous automata RWTH record for Model checking pPDA vs unambiguous automata BibTeX for Model checking pPDA vs unambiguous automata
Bachelor’s thesis
Application of Reinforcement Learning to the Game of Reversi++
Songran Shi
RWTH Aachen University
Advisers: Thomas Noll, Bastian Leibe
Consultants: Christopher Jan-Steffen Brix
PDF of Application of Reinforcement Learning to the Game of Reversi++RWTH record for Application of Reinforcement Learning to the Game of Reversi++BibTeX for Application of Reinforcement Learning to the Game of Reversi++
Master’s thesis
Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning
Johannes Lehmann
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning RWTH record for Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning BibTeX for Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning
Bachelor’s thesis
Proving termination of probabilistic recursive programs via SMT-solving
Leo Mommers
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Erika Ábrahám
Consultants: Tobias Winkler
PDF of Proving termination of probabilistic recursive programs via SMT-solving RWTH record for Proving termination of probabilistic recursive programs via SMT-solving BibTeX for Proving termination of probabilistic recursive programs via SMT-solving
Bachelor’s thesis
Compositional control-flow reduction for probabilistic model checking
Naomi Barth
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Compositional control-flow reduction for probabilistic model checking RWTH record for Compositional control-flow reduction for probabilistic model checking BibTeX for Compositional control-flow reduction for probabilistic model checking
Master’s thesis
Invariant-based strategy synthesis for nondeterministic probabilistic programs
Tom Biskup
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
PDF of Invariant-based strategy synthesis for nondeterministic probabilistic programs RWTH record for Invariant-based strategy synthesis for nondeterministic probabilistic programs BibTeX for Invariant-based strategy synthesis for nondeterministic probabilistic programs
Master’s thesis
Complexity and decidability of multi-objective stochastic games
Tobias Winkler
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Jan Křetínský
Consultants: Maximilian Weininger
PDF of Complexity and decidability of multi-objective stochastic games RWTH record for Complexity and decidability of multi-objective stochastic games BibTeX for Complexity and decidability of multi-objective stochastic games
Bachelor’s thesis
Combining integer programs and graph grammars: Theory and implementation in Attestor
Alexander Ferber
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
PDF of Combining integer programs and graph grammars: Theory and implementation in Attestor RWTH record for Combining integer programs and graph grammars: Theory and implementation in Attestor BibTeX for Combining integer programs and graph grammars: Theory and implementation in Attestor

2023

Master’s thesis
Evaluation of out-of-distribution detection techniques for dataset filtering
Lasse van der Woude
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Evaluation of out-of-distribution detection techniques for dataset filtering BibTeX for Evaluation of out-of-distribution detection techniques for dataset filtering
Bachelor’s thesis
Automated assessment of regular expressions
Ebru Kusak
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Automated assessment of regular expressions BibTeX for Automated assessment of regular expressions
Master’s thesis
Architecture-oriented safety verification of transformer networks via program analysis
Daniel Alexander Heinen
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Architecture-oriented safety verification of transformer networks via program analysis BibTeX for Architecture-oriented safety verification of transformer networks via program analysis
Bachelor’s thesis
Slicing COBOL software for program understanding
Stefan Busch
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Slicing COBOL software for program understanding BibTeX for Slicing COBOL software for program understanding
Master’s thesis
Approximate probabilistic bisimulations and quotienting
Timm Spork
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Approximate probabilistic bisimulations and quotienting BibTeX for Approximate probabilistic bisimulations and quotienting
Master’s thesis
Representing Markov models by extending the intermediate model checking language
Jialei Yao
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Representing Markov models by extending the intermediate model checking language BibTeX for Representing Markov models by extending the intermediate model checking language
Bachelor’s thesis
Automatic algorithm selection for probabilistic model checking using machine learning
Umut Yigit Dural
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann, Alexander Nikolai Bork
RWTH record for Automatic algorithm selection for probabilistic model checking using machine learning BibTeX for Automatic algorithm selection for probabilistic model checking using machine learning
Bachelor’s thesis
Strategy computation for a Markovian disease spread model
Gergana Tropcheva
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Alexander Nikolai Bork
RWTH record for Strategy computation for a Markovian disease spread model BibTeX for Strategy computation for a Markovian disease spread model
PhD thesis
Monotonicity in Markov models
Jip Josephine Spel
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Tatjana Petrov
PDF of Monotonicity in Markov models RWTH record for Monotonicity in Markov models BibTeX for Monotonicity in Markov models
Bachelor’s thesis
Comparison of symbolic maximal end component decomposition algorithms
Felix Faber
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Comparison of symbolic maximal end component decomposition algorithms BibTeX for Comparison of symbolic maximal end component decomposition algorithms
PhD thesis
Verification of multi-objective Markov models
Tim Quatmann
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Mickael Randour
PDF of Verification of multi-objective Markov models RWTH record for Verification of multi-objective Markov models BibTeX for Verification of multi-objective Markov models
PhD thesis
Synthesizing FDIR recovery strategies for space systems
Sascha Müller
RWTH Aachen University
Advisers: Thomas Noll, Andreas Gerndt, Joost-Pieter Katoen
PDF of Synthesizing FDIR recovery strategies for space systems RWTH record for Synthesizing FDIR recovery strategies for space systems BibTeX for Synthesizing FDIR recovery strategies for space systems

2022

Bachelor’s thesis
Implementation of an LTL model checker for probabilistic pushdown automata
Laura Bamberger
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
RWTH record for Implementation of an LTL model checker for probabilistic pushdown automata BibTeX for Implementation of an LTL model checker for probabilistic pushdown automata
Master’s thesis
Inference in discrete probabilistic programs using probability generating functions
Christian Blumenthal
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Lutz Klinkenberg, Tobias Winkler
RWTH record for Inference in discrete probabilistic programs using probability generating functions BibTeX for Inference in discrete probabilistic programs using probability generating functions
Bachelor’s thesis
Automatic verification of loop invariants in weighted programs
Ben Sturgis
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler, Kevin Batz
RWTH record for Automatic verification of loop invariants in weighted programs BibTeX for Automatic verification of loop invariants in weighted programs
Master’s thesis
Novelty-detection-based split selection heuristics for neural network verification
Caroline Jabs
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix, Marcel Moosbrugger
RWTH record for Novelty-detection-based split selection heuristics for neural network verification BibTeX for Novelty-detection-based split selection heuristics for neural network verification
Bachelor’s thesis
Comparison of heuristics for branching in neural network verification
Jonas Seidel
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Comparison of heuristics for branching in neural network verification BibTeX for Comparison of heuristics for branching in neural network verification
Master’s thesis
POMDP-based execution models for probabilistic programs with partial observability
Christina Gehnen
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Alexander Nikolai Bork, Tobias Winkler
PDF of POMDP-based execution models for probabilistic programs with partial observability RWTH record for POMDP-based execution models for probabilistic programs with partial observability BibTeX for POMDP-based execution models for probabilistic programs with partial observability
Bachelor’s thesis
Verifying parametric Markov models using decision diagrams
Jan Erik Karuc
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Verifying parametric Markov models using decision diagrams BibTeX for Verifying parametric Markov models using decision diagrams
Master’s thesis
Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung
Denis Kuksaus
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung BibTeX for Markow-Entscheidungsprozesse mit mehreren Agenten : Ein Überblick mit Fokus auf effiziente Aufgabenverteilung
PhD thesis
Dynamic fault trees: semantics, analysis and applications
Matthias Volk
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Alessandro Cimatti
PDF of Dynamic fault trees: semantics, analysis and applications RWTH record for Dynamic fault trees: semantics, analysis and applications BibTeX for Dynamic fault trees: semantics, analysis and applications
Bachelor’s thesis
Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation
Dominic Sebastian Meiser
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
RWTH record for Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation BibTeX for Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation
Bachelor’s thesis
Verification of leader election protocols for dynamic networks
Jan Jeremy Tugsbayar
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
RWTH record for Verification of leader election protocols for dynamic networks BibTeX for Verification of leader election protocols for dynamic networks
PhD thesis
Boolean-logic driven Markov processes : Explained. Analysed. Verified.
Shahid Khan
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Mariëlle Ida Antoinette Stoelinga
PDF of Boolean-logic driven Markov processes : Explained. Analysed. Verified.RWTH record for Boolean-logic driven Markov processes : Explained. Analysed. Verified.BibTeX for Boolean-logic driven Markov processes : Explained. Analysed. Verified.
Master’s thesis
Termination analysis of procedural pointer programs modelled by graph grammars
Mohamed Khalifa
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
PDF of Termination analysis of procedural pointer programs modelled by graph grammars RWTH record for Termination analysis of procedural pointer programs modelled by graph grammars BibTeX for Termination analysis of procedural pointer programs modelled by graph grammars
Bachelor’s thesis
Verification of neural networks using binary tree search for branching
Lisa Pühl
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Christopher Jan-Steffen Brix
RWTH record for Verification of neural networks using binary tree search for branching BibTeX for Verification of neural networks using binary tree search for branching
Master’s thesis
A unified slicing framework for probabilistic programs
Darion Haase
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for A unified slicing framework for probabilistic programs BibTeX for A unified slicing framework for probabilistic programs

2021

Bachelor’s thesis
Automata-based model checking of recursive systems
Christina Gehnen
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tobias Winkler
PDF of Automata-based model checking of recursive systems RWTH record for Automata-based model checking of recursive systems BibTeX for Automata-based model checking of recursive systems
Master’s thesis
Underapproximations for indefinite-horizon POMDPS
Alexander Nikolai Bork
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Gerhard Lakemeyer
Consultants: Tim Quatmann
RWTH record for Underapproximations for indefinite-horizon POMDPS BibTeX for Underapproximations for indefinite-horizon POMDPS
Bachelor’s thesis
Analysis of concurrent probabilistic programs with shared variables
Fabian Gasser
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
Consultants: Ira Justus Fesefeldt
RWTH record for Analysis of concurrent probabilistic programs with shared variables BibTeX for Analysis of concurrent probabilistic programs with shared variables
Master’s thesis
Decidability and complexity of entailment checking in quantitative separation logic
Marvin Jansen
RWTH Aachen University
Advisers: Kevin Batz, Ira Justus Fesefeldt, Christoph Matheja, Joost-Pieter Katoen, Thomas Noll
RWTH record for Decidability and complexity of entailment checking in quantitative separation logic BibTeX for Decidability and complexity of entailment checking in quantitative separation logic
Bachelor’s thesis
Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs
Patrick Arens
RWTH Aachen University
Advisers: Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll
RWTH record for Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs BibTeX for Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs
Master’s thesis
IDE-Ready parsing of compile-time dynamic languages
Domenic Quirl
RWTH Aachen University
Advisers: Thomas Noll
RWTH record for IDE-Ready parsing of compile-time dynamic languages BibTeX for IDE-Ready parsing of compile-time dynamic languages
Master’s thesis
Efficient analysis of time-bounded reachability in markov automata
Mengying Xue
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Tim Quatmann
RWTH record for Efficient analysis of time-bounded reachability in markov automata BibTeX for Efficient analysis of time-bounded reachability in markov automata
Bachelor’s thesis
Learning probabilistic automata with SMT solving
Dario Veltri
RWTH Aachen University
Advisers: Joshua Moerman, Joost-Pieter Katoen, Thomas Noll
PDF of Learning probabilistic automata with SMT solving RWTH record for Learning probabilistic automata with SMT solving BibTeX for Learning probabilistic automata with SMT solving

2020

Master’s thesis
Parameter synthesis in bayesian networks
Robin Drahovsky
RWTH Aachen University
Advisers: Bahare Salmani Barzoki, Joost-Pieter Katoen, Thomas Noll
RWTH record for Parameter synthesis in bayesian networks BibTeX for Parameter synthesis in bayesian networks
Master’s thesis
A petri net semantics for boolean-logic driven markov processes
Lars Beckers
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Shahid Khan
RWTH record for A petri net semantics for boolean-logic driven markov processes BibTeX for A petri net semantics for boolean-logic driven markov processes
Bachelor’s thesis
Dynamic fault tree analysis using binary decision diagrams
Daniel Basgöze
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll
Consultants: Matthias Volk, Shahid Khan
PDF of Dynamic fault tree analysis using binary decision diagrams RWTH record for Dynamic fault tree analysis using binary decision diagrams BibTeX for Dynamic fault tree analysis using binary decision diagrams
Master’s thesis
Parameter synthesis in probabilistic timed automata
Bram Kohlen
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Erika Ábrahám
Consultants: Jip Josephine Spel
RWTH record for Parameter synthesis in probabilistic timed automata BibTeX for Parameter synthesis in probabilistic timed automata
Bachelor’s thesis
RPrIC3: PrIC3 for expected rewards
Adrian Gallus
RWTH Aachen University
Advisers: Kevin Batz, Joost-Pieter Katoen, Thomas Noll
RWTH record for RPrIC3: PrIC3 for expected rewards BibTeX for RPrIC3: PrIC3 for expected rewards
Bachelor’s thesis
Implementation of a Predicate-Guided Termination Analysis for Pointer Programs
Mohamed Khalifa
RWTH Aachen University
Advisers: Ira Justus Fesefeldt, Thomas Noll, Joost-Pieter Katoen
PDF of Implementation of a Predicate-Guided Termination Analysis for Pointer Programs RWTH record for Implementation of a Predicate-Guided Termination Analysis for Pointer Programs BibTeX for Implementation of a Predicate-Guided Termination Analysis for Pointer Programs
Bachelor’s thesis
Gradient descent on parametric Markov Chains
Linus Heck
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Thomas Noll, Jip Josephine Spel
PDF of Gradient descent on parametric Markov Chains RWTH record for Gradient descent on parametric Markov Chains BibTeX for Gradient descent on parametric Markov Chains
Master’s thesis
Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds
Christopher Brix
RWTH Aachen University
Advisers: Thomas Noll
RWTH record for Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds BibTeX for Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds
Master’s thesis
Design and implementation of an interactive exploration tool for probabilistic programs
Alexander Hoppen
RWTH Aachen University
Advisers: Thomas Noll, Joost-Pieter Katoen
RWTH record for Design and implementation of an interactive exploration tool for probabilistic programs BibTeX for Design and implementation of an interactive exploration tool for probabilistic programs
Bachelor’s thesis
Quantitative Analysis of Counterexample Generation for Automata Learning
Dan-Tuong Le
RWTH Aachen University
Advisers: Joshua Moerman, Joost-Pieter Katoen, Thomas Noll
PDF of Quantitative Analysis of Counterexample Generation for Automata Learning RWTH record for Quantitative Analysis of Counterexample Generation for Automata Learning BibTeX for Quantitative Analysis of Counterexample Generation for Automata Learning
Bachelor’s thesis
Learning RFSA in Reverse
Thomas Vogt
RWTH Aachen University
Advisers: Joshua Moerman, Joost-Pieter Katoen, Thomas Noll
RWTH record for Learning RFSA in Reverse BibTeX for Learning RFSA in Reverse
PhD thesis
Optimal planning modulo theories
Francesco Leofante
RWTH Aachen University
Advisers: Erika Ábrahám, Armando Tacchella
PDF of Optimal planning modulo theories RWTH record for Optimal planning modulo theories BibTeX for Optimal planning modulo theories
PhD thesis
Parameter synthesis in Markov models
Sebastian Junges
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Alessandro Abate, Javier Esparza
PDF of Parameter synthesis in Markov models RWTH record for Parameter synthesis in Markov models BibTeX for Parameter synthesis in Markov models
PhD thesis
Automated reasoning and randomization in separation logic
Christoph Matheja
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Radu Iosif
PDF of Automated reasoning and randomization in separation logic RWTH record for Automated reasoning and randomization in separation logic BibTeX for Automated reasoning and randomization in separation logic

2019

Master’s thesis
Proving termination of pointer programs on top of symbolic execution
Ira Justus Fesefeldt
RWTH Aachen University
Advisers: Christoph Matheja, Thomas Noll, Joost-Pieter Katoen
PDF of Proving termination of pointer programs on top of symbolic execution RWTH record for Proving termination of pointer programs on top of symbolic execution BibTeX for Proving termination of pointer programs on top of symbolic execution
PhD thesis
State set representations and their usage in the reachability analysis of hybrid systems
Stefan Schupp
RWTH Aachen University
Advisers: Erika Ábrahám, Goran Frehse
PDF of State set representations and their usage in the reachability analysis of hybrid systems RWTH record for State set representations and their usage in the reachability analysis of hybrid systems BibTeX for State set representations and their usage in the reachability analysis of hybrid systems
PhD thesis
New results on probabilistic verification : automata, logic and satisfiability
Souymodip Chakraborty
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Lijun Zhang
PDF of New results on probabilistic verification : automata, logic and satisfiability RWTH record for New results on probabilistic verification : automata, logic and satisfiability BibTeX for New results on probabilistic verification : automata, logic and satisfiability
PhD thesis
Advanced weakest precondition calculi for probabilistic programs
Benjamin Lucien Kaminski
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Annabelle McIver
PDF of Advanced weakest precondition calculi for probabilistic programs RWTH record for Advanced weakest precondition calculi for probabilistic programs BibTeX for Advanced weakest precondition calculi for probabilistic programs

2018

PhD thesis
Model-based reliability analysis of aerospace systems
Harold Yorick Bruintjes
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Alessandro Cimatti
PDF of Model-based reliability analysis of aerospace systems RWTH record for Model-based reliability analysis of aerospace systems BibTeX for Model-based reliability analysis of aerospace systems
PhD thesis
IC3 software model checking
Tim Felix Lange
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Georg Weissenbacher, Martin R. Neuhäußer
PDF of IC3 software model checking RWTH record for IC3 software model checking BibTeX for IC3 software model checking
PhD thesis
On solving real-algebraic formulas in a satisfiability-modulo-theories framework
Ulrich Loup
RWTH Aachen University
Advisers: Erika Ábrahám, Viktor Levandovskyy, Thomas Sturm
PDF of On solving real-algebraic formulas in a satisfiability-modulo-theories framework RWTH record for On solving real-algebraic formulas in a satisfiability-modulo-theories framework BibTeX for On solving real-algebraic formulas in a satisfiability-modulo-theories framework
PhD thesis
The probabilistic model checker Storm : symbolic methods for probabilistic model checking
Hans Christian Hensel
RWTH Aachen University
Advisers: Joost-Pieter Katoen, David Parker
PDF of The probabilistic model checker Storm : symbolic methods for probabilistic model checking RWTH record for The probabilistic model checker Storm : symbolic methods for probabilistic model checking BibTeX for The probabilistic model checker Storm : symbolic methods for probabilistic model checking

2017

2016

PhD thesis
Integrating virtual substitution into strategic SMT solving
Florian Corzilius
RWTH Aachen University
Advisers: Erika Ábrahám, Pascal Fontaine
PDF of Integrating virtual substitution into strategic SMT solving RWTH record for Integrating virtual substitution into strategic SMT solving BibTeX for Integrating virtual substitution into strategic SMT solving
PhD thesis
Semantics and loop invariant synthesis for probabilistic programs
Friedrich Gretz
Aachen, Techn. Hochsch.
Advisers: Joost-Pieter Katoen, Sriram Sankaranarayanan
PDF of Semantics and loop invariant synthesis for probabilistic programs RWTH record for Semantics and loop invariant synthesis for probabilistic programs BibTeX for Semantics and loop invariant synthesis for probabilistic programs

2015

PhD thesis
Verifying Java programs : a graph grammar approach
Jonathan Heinen
Verl. Dr. Hut
Advisers: Joost-Pieter Katoen, Arend Rensink
RWTH record for Verifying Java programs : a graph grammar approach BibTeX for Verifying Java programs : a graph grammar approach
PhD thesis
Counterexamples in probabilistic verification
Nils Jansen
Aachen, Techn. Hochsch.
Advisers: Erika Ábrahám, Bernd Becker, Joost-Pieter Katoen
PDF of Counterexamples in probabilistic verification RWTH record for Counterexamples in probabilistic verification BibTeX for Counterexamples in probabilistic verification
PhD thesis
Abstraction and refinement of probabilistic automata using modal stochastic games
Falak Sher
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Lijun Zhang
PDF of Abstraction and refinement of probabilistic automata using modal stochastic games RWTH record for Abstraction and refinement of probabilistic automata using modal stochastic games BibTeX for Abstraction and refinement of probabilistic automata using modal stochastic games
PhD thesis
Reduction Techniques for Nondeterministic and Probabilistic Systems
Arpit Sharma
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Holger Hermanns
PDF of Reduction Techniques for Nondeterministic and Probabilistic Systems RWTH record for Reduction Techniques for Nondeterministic and Probabilistic Systems BibTeX for Reduction Techniques for Nondeterministic and Probabilistic Systems

2014

PhD thesis
Verifying probabilistic systems : new algorithms and complexity results
Hongfei Fu
Zugl.: Aachen, Techn. Hochsch.
Advisers: Joost-Pieter Katoen
PDF of Verifying probabilistic systems : new algorithms and complexity results RWTH record for Verifying probabilistic systems : new algorithms and complexity results BibTeX for Verifying probabilistic systems : new algorithms and complexity results

2013

PhD thesis
Trustworthy spacecraft design using formal methods
Viet Yen Nguyen
Dep. of Computer Science, RWTH Aachen
Advisers: Joost-Pieter Katoen
PDF of Trustworthy spacecraft design using formal methods RWTH record for Trustworthy spacecraft design using formal methods BibTeX for Trustworthy spacecraft design using formal methods
PhD thesis
Analyzing energy consumption of wireless networks : a model-based approach
Haidi Yue
Publikationsserver der RWTH Aachen University
Advisers: Joost-Pieter Katoen
PDF of Analyzing energy consumption of wireless networks : a model-based approach RWTH record for Analyzing energy consumption of wireless networks : a model-based approach BibTeX for Analyzing energy consumption of wireless networks : a model-based approach

2011

Master’s thesis
Static byte-code analysis for state space reduction
Gustavo Quirós Araya
Publikationsserver der RWTH Aachen University
PDF of Static byte-code analysis for state space reduction RWTH record for Static byte-code analysis for state space reduction BibTeX for Static byte-code analysis for state space reduction

2010

PhD thesis
Three-valued abstraction for stochastic systems
Daniel Klink
Hut
Advisers: Joost-Pieter Katoen
PDF of Three-valued abstraction for stochastic systems RWTH record for Three-valued abstraction for stochastic systems BibTeX for Three-valued abstraction for stochastic systems

2009

PhD thesis
Diagnosis, synthesis and analysis of probabilistic models
Tingting Han
Univ. Twente
Advisers: Joost-Pieter Katoen
PDF of Diagnosis, synthesis and analysis of probabilistic models RWTH record for Diagnosis, synthesis and analysis of probabilistic models BibTeX for Diagnosis, synthesis and analysis of probabilistic models
PhD thesis
Verification of pointer programs
Stefan Rieger
Publikationsserver der RWTH Aachen University
Advisers: Joost-Pieter Katoen
PDF of Verification of pointer programs RWTH record for Verification of pointer programs BibTeX for Verification of pointer programs
PhD thesis
Learning communicating and nondeterministic automata
Carsten Kern
RWTH Aachen, Department of Computer Science
Advisers: Joost-Pieter Katoen
PDF of Learning communicating and nondeterministic automata RWTH record for Learning communicating and nondeterministic automata BibTeX for Learning communicating and nondeterministic automata

2006

PhD thesis
Parallel algorithms for verification of large systems
Michael Weber
RWTH, Department of Computer Science
Advisers: Klaus Indermark
PDF of Parallel algorithms for verification of large systems RWTH record for Parallel algorithms for verification of large systems BibTeX for Parallel algorithms for verification of large systems

1998

PhD thesis
High level parallel programming and the efficient implementation of numerical algorithms
George Horatiu Botorog
RWTH, Fachgruppe Informatik
Advisers: Klaus Indermark, Friedel Hoßfeld
RWTH record for High level parallel programming and the efficient implementation of numerical algorithms BibTeX for High level parallel programming and the efficient implementation of numerical algorithms

1997

PhD thesis
Optimising the memory management of higher order functional programs
Markus Mohnen
RWTH, Fachgruppe Informatik
Advisers: K. Indermark, R. Plasmeijer
RWTH record for Optimising the memory management of higher order functional programs BibTeX for Optimising the memory management of higher order functional programs