Theses (Co-)Supervised by Thomas Noll

2026

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

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
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
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
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
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
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
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
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
Bachelor’s thesis
Evaluating static analysis techniques to accelerate data race detection for MPI RMA
Yussur Mustafa Oraji
RWTH Aachen University
Advisers: Matthias S. Müller, Thomas Noll
Consultants: Simon Schwitanski
PDF of Evaluating static analysis techniques to accelerate data race detection for MPI RMA RWTH record for Evaluating static analysis techniques to accelerate data race detection for MPI RMA BibTeX for Evaluating static analysis techniques to accelerate data race detection for MPI RMA

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
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
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
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
Developing an on-the-fly vector clock exchange for distributed memory systems using the generic tool infrastructure
Felix Tomski
RWTH Aachen University
Advisers: Matthias S. Müller, Thomas Noll
Consultants: Simon Schwitanski
RWTH record for Developing an on-the-fly vector clock exchange for distributed memory systems using the generic tool infrastructure BibTeX for Developing an on-the-fly vector clock exchange for distributed memory systems using the generic tool infrastructure
Master’s thesis
Accelerating symbolic simulation to analyze the effect of delays in train timetables
Niklas Kotowski
RWTH Aachen University
Advisers: Erika Ábrahám, Thomas Noll
Consultants: Rebecca Haehn
PDF of Accelerating symbolic simulation to analyze the effect of delays in train timetables RWTH record for Accelerating symbolic simulation to analyze the effect of delays in train timetables BibTeX for Accelerating symbolic simulation to analyze the effect of delays in train timetables
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
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

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

2017

PhD thesis
Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic
Christina Jansen
RWTH Aachen University
Advisers: Joost-Pieter Katoen, Marieke Huisman, Thomas Noll
PDF of Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic RWTH record for Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic BibTeX for Static Analysis of Pointer Programs - Linking Graph Grammars and Separation Logic