Thomas Noll

Photo of Thomas Noll

Email: noll@cs.rwth-aachen.de
Address: Room 4211 (Faculty of CS, building E1 (2353), 2nd floor)
Ahornstraße 55
D-52074 Aachen
Phone: +49 241 80 21213

I am an associate professor (apl. Prof.) at the Software Modeling and Verification Group (MOVES), headed by Prof. Joost-Pieter Katoen, in the Faculty of Computer Science at RWTH Aachen University. The office is located at the Computer Science Center. My current research interests include:

Static Program Analysis for Software Optimisation and Verification
Compilation of Quantum Circuits
Reliability, Safety and Security of Hardware/Software Systems
Formal Verification of Artificial Neural Networks

Publications

Own publications

2025

2023

Proceedings
22. Kolloquium Programmiersprachen und Grundlagen der Programmierung
RWTH Aachen University, Department of Computer Science
PDF of 22. Kolloquium Programmiersprachen und Grundlagen der Programmierung RWTH record for 22. Kolloquium Programmiersprachen und Grundlagen der Programmierung BibTeX for 22. Kolloquium Programmiersprachen und Grundlagen der Programmierung

2022

Conference paper
Identification of Bottlenecks in Rail Infrastructure
Wiebke Lenze, Bastian Kogel, Simon Schotten, Thorsten Büker, Thomas Noll, Philipp Berger, Mario Fietze
Proceedings of the Fifth International Conference on Railway Technology: Research, Development and Maintenance Edited by J. Pombo Civil-Comp Conferences. - Volume 1
RWTH record for Identification of Bottlenecks in Rail Infrastructure BibTeX for Identification of Bottlenecks in Rail Infrastructure
Conference paper
Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining
Philipp Berger, Wiebke Lenze, Thomas Noll, Simon Schotten, Thorsten Büker, Mario Fietze, Bastian Kogel
Formal Methods for Industrial Critical Systems
RWTH record for Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining BibTeX for Analysing Capacity Bottlenecks in Rail Infrastructure by Episode Mining
Technical report
50 Jahre Studiengang Informatik an der RWTH Aachen : Ein Streifzug in Text und Bild
RWTH record for 50 Jahre Studiengang Informatik an der RWTH Aachen : Ein Streifzug in Text und Bild BibTeX for 50 Jahre Studiengang Informatik an der RWTH Aachen : Ein Streifzug in Text und Bild
Preprint
Towards Concurrent Quantitative Separation Logic
Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll
PDF of Towards Concurrent Quantitative Separation Logic RWTH record for Towards Concurrent Quantitative Separation Logic BibTeX for Towards Concurrent Quantitative Separation Logic
Conference paper
Towards Concurrent Quantitative Separation Logic
Ira Justus Fesefeldt, Joost-Pieter Katoen, Thomas Noll
33rd International Conference on Concurrency Theory (CONCUR 2022)
PDF of Towards Concurrent Quantitative Separation Logic RWTH record for Towards Concurrent Quantitative Separation Logic BibTeX for Towards Concurrent Quantitative Separation Logic
Journal article
Einblick DZSF-Projekt "Identifikation von Kapazitätsengpässen"
Simon Schotten, Thorsten Büker, Wiebke Lenze, Bastian Kogel, Thomas Noll, Mario Fietze, Jana Berger
Eisenbahntechnische Rundschau
RWTH record for Einblick DZSF-Projekt "Identifikation von Kapazitätsengpässen"BibTeX for Einblick DZSF-Projekt "Identifikation von Kapazitätsengpässen"
Conference paper
Foundations for Entailment Checking in Quantitative Separation Logic
Kevin Batz, Ira Justus Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja, Thomas Noll
Programming Languages and Systems
PDF of Foundations for Entailment Checking in Quantitative Separation Logic RWTH record for Foundations for Entailment Checking in Quantitative Separation Logic BibTeX for Foundations for Entailment Checking in Quantitative Separation Logic

2021

Conference paper
A Debugger for Probabilistic Programs
Alexander Hoppen, Thomas Noll
Software Engineering and Formal Methods
RWTH record for A Debugger for Probabilistic Programs BibTeX for A Debugger for Probabilistic Programs
Conference paper
A Modular Approach to Non-deterministic Dynamic Fault Trees
Sascha Müller, Adeline Jordon, Andreas Gerndt, Thomas Noll
Computer Safety, Reliability, and Security
RWTH record for A Modular Approach to Non-deterministic Dynamic Fault Trees BibTeX for A Modular Approach to Non-deterministic Dynamic Fault Trees
Conference paper
Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars
Ira Justus Fesefeldt, Christoph Matheja, Thomas Noll, Johannes Schulte
Graph Transformation
RWTH record for Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars BibTeX for Automated Checking and Completion of Backward Confluence for Hyperedge Replacement Grammars

2020

Journal article
Synthesizing and optimizing FDIR recovery strategies from fault trees
Sascha Müller, Liana Mikaelyan, Andreas Gerndt, Thomas Noll
Science of computer programming
PDF of Synthesizing and optimizing FDIR recovery strategies from fault trees RWTH record for Synthesizing and optimizing FDIR recovery strategies from fault trees BibTeX for Synthesizing and optimizing FDIR recovery strategies from fault trees
Preprint
Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs
Christopher Jan-Steffen Brix, Thomas Noll
PDF of Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs RWTH record for Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs BibTeX for Debona: Decoupled Boundary Network Analysis for Tighter Bounds and Faster Adversarial Robustness Proofs
Journal article
IC3 software model checking
Tim Felix Lange, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen
International journal on software tools for technology transfer
RWTH record for IC3 software model checking BibTeX for IC3 software model checking

2019

Conference paper
COMPASS 3.0
Marco Bozzano, Harold Yorick Bruintjes, Alessandro Cimatti, Joost-Pieter Katoen, Thomas Noll, Stefano Tonetta
Tools and algorithms for the construction and analysis of systems
PDF of COMPASS 3.0 RWTH record for COMPASS 3.0 BibTeX for COMPASS 3.0
Conference paper
Synthesizing and Optimizing FDIR Recovery Strategies from Fault Trees
Liana Mikaelyan, Sascha Müller, Andreas Gerndt, Thomas Noll
Formal techniques for safety-critical systems
RWTH record for Synthesizing and Optimizing FDIR Recovery Strategies from Fault Trees BibTeX for Synthesizing and Optimizing FDIR Recovery Strategies from Fault Trees
Journal article
Quantitative separation logic: a logic for reasoning about probabilistic pointer programs
Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja, Thomas Noll
Proceedings of the ACM on programming languages
PDF of Quantitative separation logic: a logic for reasoning about probabilistic pointer programs RWTH record for Quantitative separation logic: a logic for reasoning about probabilistic pointer programs BibTeX for Quantitative separation logic: a logic for reasoning about probabilistic pointer programs

2018

Journal article
Synthesizing Failure Detection, Isolation, and Recovery Strategies from Nondeterministic Dynamic Fault Trees
Sascha Müller, Andreas Gerndt, Thomas Noll
Journal of Aerospace Information Systems
RWTH record for Synthesizing Failure Detection, Isolation, and Recovery Strategies from Nondeterministic Dynamic Fault Trees BibTeX for Synthesizing Failure Detection, Isolation, and Recovery Strategies from Nondeterministic Dynamic Fault Trees
Conference paper
Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic
Jens Katelaan, Christoph Matheja, Thomas Noll, Florian Zuleger
LPAR-22
RWTH record for Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic BibTeX for Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic
Conference paper
Improving Generalization in Software IC3
Tim Lange, Frederick Prinz, Martin R. Neuhäußer, Thomas Noll, Joost-Pieter Katoen
Model checking software
RWTH record for Improving Generalization in Software IC3 BibTeX for Improving Generalization in Software IC3

Supervised theses

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

All records on RWTH Publications