Theses (Co-)Supervised by Thomas Noll

2024
DOI fulltext PDF [bibtex]
@masterthesis{CTA2024,
title = {Combining integer programs and graph grammars: Theory and implementation in Attestor},
author = {Alexander Ferber},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-00784},
url = { https://publications.rwth-aachen.de/record/977552},
}×
[issue]
Alexander Ferber. Combining integer programs and graph grammars: Theory and implementation in Attestor, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{I2024,
title = {Invariant-based strategy synthesis for nondeterministic probabilistic programs},
author = {Tom Biskup},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02594},
url = { https://publications.rwth-aachen.de/record/980850},
}×
[issue]
Tom Biskup. Invariant-based strategy synthesis for nondeterministic probabilistic programs, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{C2024,
title = {Compositional control-flow reduction for probabilistic model checking},
author = {Naomi Barth},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02596},
url = { https://publications.rwth-aachen.de/record/980852},
}×
[issue]
Naomi Barth. Compositional control-flow reduction for probabilistic model checking, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{P2024,
title = {Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning},
author = {Johannes Lehmann},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02603},
url = { https://publications.rwth-aachen.de/record/980859},
}×
[issue]
Johannes Lehmann. Pushdown and expectation transformer semantics of probabilistic recursive programs with nested conditioning, Master Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{ARLGR2024,
title = {Application of Reinforcement Learning to the Game of Reversi++},
author = {Songran Shi},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-04092},
url = { https://publications.rwth-aachen.de/record/984514},
}×
[issue]
Songran Shi. Application of Reinforcement Learning to the Game of Reversi++, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
2023
[bibtex]
@masterthesis{C2023,
title = {Comparison of symbolic maximal end component decomposition algorithms},
author = {Felix Faber},
institution = {RWTH Aachen University},
pages = {61 Seiten : Illustrationen, Diagramme},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/974509},
}×
[issue]
Felix Faber. Comparison of symbolic maximal end component decomposition algorithms, Bachelor Thesis, RWTH Aachen University, 61 Seiten : Illustrationen, Diagramme, 2023.
[bibtex]
@masterthesis{SM2023,
title = {Strategy computation for a Markovian disease spread model},
author = {Gergana Tropcheva},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977478},
}×
[issue]
Gergana Tropcheva. Strategy computation for a Markovian disease spread model, Bachelor Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{A2023,
title = {Automatic algorithm selection for probabilistic model checking using machine learning},
author = {Umut Yigit Dural},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977479},
}×
[issue]
Umut Yigit Dural. Automatic algorithm selection for probabilistic model checking using machine learning, Bachelor Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{RM2023,
title = {Representing Markov models by extending the intermediate model checking language},
author = {Jialei Yao},
institution = {RWTH Aachen University},
pages = {67 Seiten : Illustrationen},
type = {Master Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977529},
}×
[issue]
Jialei Yao. Representing Markov models by extending the intermediate model checking language, Master Thesis, RWTH Aachen University, 67 Seiten : Illustrationen, 2023.
[bibtex]
@masterthesis{A2023,
title = {Approximate probabilistic bisimulations and quotienting},
author = {Timm Spork},
institution = {RWTH Aachen University},
pages = {186 Seiten : Illustrationen},
type = {Master Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977530},
}×
[issue]
Timm Spork. Approximate probabilistic bisimulations and quotienting, Master Thesis, RWTH Aachen University, 186 Seiten : Illustrationen, 2023.
[bibtex]
@masterthesis{SC2023,
title = {Slicing COBOL software for program understanding},
author = {Stefan Busch},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977551},
}×
[issue]
Stefan Busch. Slicing COBOL software for program understanding, Bachelor Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{A2023,
title = {Architecture-oriented safety verification of transformer networks via program analysis},
author = {Daniel Alexander Heinen},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977553},
}×
[issue]
Daniel Alexander Heinen. Architecture-oriented safety verification of transformer networks via program analysis, Master Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{A2023,
title = {Automated assessment of regular expressions},
author = {Ebru Kusak},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977555},
}×
[issue]
Ebru Kusak. Automated assessment of regular expressions, Bachelor Thesis, RWTH Aachen University, 2023.
[bibtex]
@masterthesis{E2023,
title = {Evaluation of out-of-distribution detection techniques for dataset filtering},
author = {Lasse van der Woude},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2023},
url = { https://publications.rwth-aachen.de/record/977559},
}×
[issue]
Lasse van der Woude. Evaluation of out-of-distribution detection techniques for dataset filtering, Master Thesis, RWTH Aachen University, 2023.
2022
[bibtex]
@masterthesis{A2022,
title = {A unified slicing framework for probabilistic programs},
author = {Darion Haase},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/847345},
}×
[issue]
Darion Haase. A unified slicing framework for probabilistic programs, Master Thesis, RWTH Aachen University, 2022.
[bibtex]
@masterthesis{V2022,
title = {Verification of neural networks using binary tree search for branching},
author = {Lisa Pühl},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/847346},
}×
[issue]
Lisa Pühl. Verification of neural networks using binary tree search for branching, Bachelor Thesis, RWTH Aachen University, 2022.
DOI fulltext PDF [bibtex]
@masterthesis{T2022,
title = {Termination analysis of procedural pointer programs modelled by graph grammars},
author = {Mohamed Khalifa},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Diagramme},
type = {Master Thesis},
year = {2022},
doi = {10.18154/RWTH-2022-09096},
url = { https://publications.rwth-aachen.de/record/853842},
}×
[issue]
Mohamed Khalifa. Termination analysis of procedural pointer programs modelled by graph grammars, Master Thesis, RWTH Aachen University, 1 Online-Ressource : Diagramme, RWTH Aachen University, 2022.
[bibtex]
@masterthesis{V2022,
title = {Verification of leader election protocols for dynamic networks},
author = {Jan Jeremy Tugsbayar},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/889042},
}×
[issue]
Jan Jeremy Tugsbayar. Verification of leader election protocols for dynamic networks, Bachelor Thesis, RWTH Aachen University, 2022.
[bibtex]
@masterthesis{DMC2022,
title = {Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation},
author = {Dominic Sebastian Meiser},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/889043},
}×
[issue]
Dominic Sebastian Meiser. Design and evaluation of a probabilistic pointer programming language using Monte-Carlo simulation, Bachelor Thesis, RWTH Aachen University, 2022.
[bibtex]
@masterthesis{MEAEFA2022,
title = {Markow-Entscheidungsprozesse mit mehreren Agenten: Ein Überblick mit Fokus auf effiziente Aufgabenverteilung},
author = {Denis Kuksaus},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/972070},
}×
[issue]
Denis Kuksaus. Markow-Entscheidungsprozesse mit mehreren Agenten: Ein Überblick mit Fokus auf effiziente Aufgabenverteilung, Master Thesis, RWTH Aachen University, 2022.
[bibtex]
@masterthesis{VM2022,
title = {Verifying parametric Markov models using decision diagrams},
author = {Jan Erik Karuc},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/972072},
}×
[issue]
Jan Erik Karuc. Verifying parametric Markov models using decision diagrams, Bachelor Thesis, RWTH Aachen University, 2022.
DOI fulltext PDF [bibtex]
@masterthesis{P2022,
title = {POMDP-based execution models for probabilistic programs with partial observability},
author = {Christina Gehnen},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Master Thesis},
year = {2022},
doi = {10.18154/RWTH-2024-02599},
url = { https://publications.rwth-aachen.de/record/980855},
}×
[issue]
Christina Gehnen. POMDP-based execution models for probabilistic programs with partial observability, Master Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2022.
[bibtex]
@masterthesis{N2022,
title = {Novelty-detection-based split selection heuristics for neural network verification},
author = {Caroline Jabs},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/985672},
}×
[issue]
Caroline Jabs. Novelty-detection-based split selection heuristics for neural network verification, Master Thesis, RWTH Aachen University, 2022.
2021
DOI fulltext PDF [bibtex]
@masterthesis{LS2021,
title = {Learning probabilistic automata with SMT solving},
author = {Dario Veltri},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {71 Seiten},
type = {Bachelor Thesis},
year = {2021},
doi = {10.18154/RWTH-2021-03668},
url = { https://publications.rwth-aachen.de/record/817079},
}×
[issue]
Dario Veltri. Learning probabilistic automata with SMT solving, Bachelor Thesis, RWTH Aachen University, 71 Seiten, RWTH Aachen University, 2021.
[bibtex]
@masterthesis{E2021,
title = {Efficient analysis of time-bounded reachability in markov automata},
author = {Mengying Xue},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/817764},
}×
[issue]
Mengying Xue. Efficient analysis of time-bounded reachability in markov automata, Master Thesis, RWTH Aachen University, 2021.
[bibtex]
@masterthesis{IR2021,
title = {IDE-Ready parsing of compile-time dynamic languages},
author = {Domenic Quirl},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/826214},
}×
[issue]
Domenic Quirl. IDE-Ready parsing of compile-time dynamic languages, Master Thesis, RWTH Aachen University, 2021.
[bibtex]
@masterthesis{W2021,
title = {Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs},
author = {Patrick Arens},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/829335},
}×
[issue]
Patrick Arens. Weakest-preexpectation proof rules for disjoint concurrent probabilistic programs, Bachelor Thesis, RWTH Aachen University, 2021.
[bibtex]
@masterthesis{D2021,
title = {Decidability and complexity of entailment checking in quantitative separation logic},
author = {Marvin Jansen},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/829336},
}×
[issue]
Marvin Jansen. Decidability and complexity of entailment checking in quantitative separation logic, Master Thesis, RWTH Aachen University, 2021.
[bibtex]
@masterthesis{A2021,
title = {Analysis of concurrent probabilistic programs with shared variables},
author = {Fabian Gasser},
institution = {RWTH Aachen University},
pages = {27 Seiten},
type = {Bachelor Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/840952},
}×
[issue]
Fabian Gasser. Analysis of concurrent probabilistic programs with shared variables, Bachelor Thesis, RWTH Aachen University, 27 Seiten, 2021.
DOI fulltext PDF [bibtex]
@masterthesis{A2021,
title = {Automata-based model checking of recursive systems},
author = {Christina Gehnen},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Bachelor Thesis},
year = {2021},
doi = {10.18154/RWTH-2024-02598},
url = { https://publications.rwth-aachen.de/record/980854},
}×
[issue]
Christina Gehnen. Automata-based model checking of recursive systems, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2021.
2020
[bibtex]
@masterthesis{LRR2020,
title = {Learning RFSA in Reverse},
author = {Thomas Vogt},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/792704},
}×
[issue]
Thomas Vogt. Learning RFSA in Reverse, Bachelor Thesis, RWTH Aachen University, 2020.
DOI fulltext PDF [bibtex]
@masterthesis{QACGAL2020,
title = {Quantitative Analysis of Counterexample Generation for Automata Learning},
author = {Dan-Tuong Le},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-06326},
url = { https://publications.rwth-aachen.de/record/792705},
}×
[issue]
Dan-Tuong Le. Quantitative Analysis of Counterexample Generation for Automata Learning, Bachelor Thesis, RWTH Aachen University, 2020.
[bibtex]
@masterthesis{D2020,
title = {Design and implementation of an interactive exploration tool for probabilistic programs},
author = {Alexander Hoppen},
institution = {RWTH Aachen University},
pages = {124 Seiten},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/802809},
}×
[issue]
Alexander Hoppen. Design and implementation of an interactive exploration tool for probabilistic programs, Master Thesis, RWTH Aachen University, 124 Seiten, 2020.
[bibtex]
@masterthesis{PNEIAEDNNUSPWEB2020,
title = {Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds},
author = {Christopher Brix},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/802815},
}×
[issue]
Christopher Brix. Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks Using Symbolic Propagation With Error Bounds, Master Thesis, RWTH Aachen University, 2020.
DOI fulltext PDF [bibtex]
@masterthesis{GMC2020,
title = {Gradient descent on parametric Markov Chains},
author = {Linus Heck},
institution = {RWTH Aachen University},
pages = {31 Seiten},
type = {Bachelor Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-10391},
url = { https://publications.rwth-aachen.de/record/804571},
}×
[issue]
Linus Heck. Gradient descent on parametric Markov Chains, Bachelor Thesis, RWTH Aachen University, 31 Seiten, 2020.
DOI fulltext PDF [bibtex]
@masterthesis{IPGTAPP2020,
title = {Implementation of a Predicate-Guided Termination Analysis for Pointer Programs},
author = {Mohamed Khalifa},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2020},
doi = {10.18154/RWTH-2020-10469},
url = { https://publications.rwth-aachen.de/record/804692},
}×
[issue]
Mohamed Khalifa. Implementation of a Predicate-Guided Termination Analysis for Pointer Programs, Bachelor Thesis, RWTH Aachen University, 2020.
[bibtex]
@masterthesis{RP2020,
title = {RPrIC3: PrIC3 for expected rewards},
author = {Adrian Gallus},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/805235},
}×
[issue]
Adrian Gallus. RPrIC3: PrIC3 for expected rewards, Bachelor Thesis, RWTH Aachen University, 2020.
DOI fulltext PDF [bibtex]
@masterthesis{D2020,
title = {Dynamic fault tree analysis using binary decision diagrams},
author = {Daniel Basgöze},
institution = {RWTH Aachen University},
pages = {76 Seiten},
type = {Bachelor Thesis},
year = {2020},
doi = {10.18154/RWTH-2021-03715},
url = { https://publications.rwth-aachen.de/record/817132},
}×
[issue]
Daniel Basgöze. Dynamic fault tree analysis using binary decision diagrams, Bachelor Thesis, RWTH Aachen University, 76 Seiten, 2020.
[bibtex]
@masterthesis{A2020,
title = {A petri net semantics for boolean-logic driven markov processes},
author = {Lars Beckers},
institution = {RWTH Aachen University},
pages = {55 Seiten},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/818013},
}×
[issue]
Lars Beckers. A petri net semantics for boolean-logic driven markov processes, Master Thesis, RWTH Aachen University, 55 Seiten, 2020.
[bibtex]
@masterthesis{P2020,
title = {Parameter synthesis in bayesian networks},
author = {Robin Drahovsky},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/828688},
}×
[issue]
Robin Drahovsky. Parameter synthesis in bayesian networks, Master Thesis, RWTH Aachen University, 2020.
2019
DOI fulltext PDF [bibtex]
@masterthesis{P2019,
title = {Proving termination of pointer programs on top of symbolic execution},
author = {Ira Justus Fesefeldt},
institution = {RWTH Aachen University},
pages = {118 S.},
type = {Master Thesis},
year = {2019},
doi = {10.18154/RWTH-2020-04970},
url = { https://publications.rwth-aachen.de/record/789066},
}×
[issue]
Ira Justus Fesefeldt. Proving termination of pointer programs on top of symbolic execution, Master Thesis, RWTH Aachen University, 118 S., 2019.
  • Jan Tugsbayar: Verification of Leader Election Protocols for Dynamic Networks, Bachelor Thesis, RWTH Aachen University, 2022 (co-supervisor: Ira Fesefeldt)
  • Dominic Meiser: Design and Evaluation of a Probabilistic Programming Language using Monte-Carlo Simulation, Bachelor Thesis, RWTH Aachen University, 2022 (co-supervisor: Ira Fesefeldt)
  • Xaver Fink: GNN-Based Computation of Improved Relaxations for the Verification of ReLU Neural Networks, Master Thesis, RWTH Aachen University, 2022 (supervisor: Christopher Brix)
  • Alexander Bell: Comparison of Neural Network Verification Tools, Bachelor Thesis, RWTH Aachen University, 2022 (supervisor: Christopher Brix)
  • Caroline Jabs: Novelty-Detection Based Split Selection Heuristics for Neural Network Verification, Master Thesis, RWTH Aachen University, 2022 (supervisor: Christopher Brix)
  • Annika Rüll: Identification of Repairable Regions in Deep Neural Networks, Master Thesis, RWTH Aachen University, 2022 (supervisor: Christopher Brix)
  • Jonas Seidel: Comparison of Heuristics for Branchning in Neural Network Verification, Bachelor Thesis, RWTH Aachen University, 2022 (supervisor: Christopher Brix)
  • Mohamed Khalifa: Semantics and Termination Analysis of Interprocedural Pointer Programs Modelled by Graph Grammars, Master Thesis, RWTH Aachen University, 2022 (supervisor: Ira Fesefeldt)
  • Niklas Molczanski: Verifying Recurrent Neural Networks using Frameworks for Static Program Analysis, Bachelor Thesis, RWTH Aachen University, 2022
  • Marc Wulf: Comparing Garbage Collection Methods for a Natively Compiled Functional Programming Language, Bachelor Thesis, RWTH Aachen University, 2022
  • Jona Stubbe: A Formal Semantics for a Subset of the Zig Programming Language, Master Thesis, RWTH Aachen University, 2022
  • Songran Shi: Application of Reinforcement Learning to the Game of Reversi++, Bachelor Thesis, RWTH Aachen University, 2022 (supervisors: Christopher Brix and Jana Berger)
  • Lisa Pühl: Verification of Neural Networks Using Binary Tree Search for Branching, Bachelor Thesis, RWTH Aachen University, 2022 (supervisor: Christopher Brix)
  • Darion Haase: A Unified Slicing Framework for Probabilistic Programs, Master Thesis, RWTH Aachen University, 2022
  • Fabian Gasser: Analysis of Concurrent Probabilistic Programs with Shared Variables, Bachelor Thesis, RWTH Aachen University, 2021 (co-supervisor: Ira Fesefeldt)
  • Domenic Quirl: IDE-Ready Parsing of Compile Time Dynamic Languages, Master Thesis, RWTH Aachen University, 2021
  • Mohamed Khalifa: Implementation of a Predicate-Guided Termination Analysis for Pointer Programs, Bachelor Thesis, RWTH Aachen University, 2020 (supervisor: Ira Fesefeldt, Lehrstuhl Informatik 2)
  • Christopher Brix: Proving Non-Existence of Imperceptible Adversarial Examples in Deep Neural Networks using Symbolic Propagation with Error Bounds, Master Thesis, RWTH Aachen University, 2020
  • Alexander Hoppen: Design and Implementation of an Interactive Exploration Tool for Probabilistic Programs, Master Thesis, RWTH Aachen University, 2020
  • Florian Keßler: On the Decidability of Entailment Checking in Quantitative Separation Logics, Bachelor Thesis, RWTH Aachen University, 2020
  • Tobias Wirtz: Support for Java Libraries in the Attestor Shape Analysis Tool, Bachelor Thesis, RWTH Aachen University, 2020 (co-supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Ira Justus Fesefeldt: Proving Termination of Pointer Programs on Top of Symbolic Execution, Master Thesis, RWTH Aachen University, 2019 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Johannes Schulte: Automated Detection and Completion of Confluence for Graph Grammars, Master Thesis, RWTH Aachen University, 2019 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Sally Chau: Comparing Hierarchical and On-The-Fly Model Checking for Java Pointer Programs, Master Thesis, RWTH Aachen University, 2019 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Sebastian Bartsch: Systematic Design of Efficient Online Scanners, Bachelor Thesis, RWTH Aachen University, 2019
  • Caroline Jabs: Expected Runtimes of Probabilistic Pointer Programs, Bachelor Thesis, RWTH Aachen University, 2019
  • Mirela Mileva: Minimising Mealy Machines with Dependent Inputs, Bachelor Thesis, RWTH Aachen University, 2019
  • Philipp Schroer: Understanding Abstraction of Probabilistic Programs, Bachelor Thesis, RWTH Aachen University, 2019 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Sabrina Kowarsch: Modeling a Satellite with COMPASS, Master Thesis, RWTH Aachen University, 2018 (co-supervisor: Harold Bruintjes, Lehrstuhl Informatik 2)
  • Fabian Schneider: A Unified Algebraic Domain for Shape Analysis, Master Thesis, RWTH Aachen University, 2018 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Felix Bier: From Forest Automata to Hyperedge Replacement Grammars and Back, Master Thesis, RWTH Aachen University, 2018 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Daniel Cloerkes: A Cyclic Proof System for Graph Grammar Inclusion, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Isabelle Tülleners: Graph-Based Heap Abstraction for Balanced Data Structures, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Thomas Mertens: Efficient Reuse of Learnt Information for Control-Flow Oriented IC3 Algorithms, Master Thesis, RWTH Aachen University, 2016 (supervisor: Tim Lange, Lehrstuhl Informatik 2; Dr. Neuhäußer, Siemens AG)
  • Frederick Prinz: Generalisation Methods for Control-Flow Oriented IC3 Algorithms, Master Thesis, RWTH Aachen University, 2016 (supervisor: Tim Lange, Lehrstuhl Informatik 2; Dr. Neuhäußer, Siemens AG)
  • Louis Wachtmeister: Analysing Cryptographically-Masked Information Flow Using Slicing, Bachelor Thesis, RWTH Aachen University, 2016
  • Hanna Franzen: Graph-Based Symbolic Execution for Pointer Programs with Data, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Hannah Arndt: Heap Abstraction Beyond Context-Freeness, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Raoul Schaffranek: Modelling a Purely Functional Subset of EcmaScript2015, Bachelor Thesis, RWTH Aachen University, 2016
  • Michael Beaumont: Efficient Computation of Weakest Preconditions, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Tim Lange, Lehrstuhl Informatik 2)
  • Sascha Müller: Evaluating Control-Flow-Based Inductive Model Checking Algorithms, Master Thesis, RWTH Aachen University, 2015 (supervisor: Tim Lange, Lehrstuhl Informatik 2)
  • Christoph Welzel: Thread-Modular Analysis of Heap-Manipulating Programs, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Christina Jansen, Lehrstuhl Informatik 2)
  • Jens Katelaan: Modular Analysis of Concurrent Pointer Programs, Master Thesis, RWTH Aachen University, 2015 (co-supervisor: Christina Jansen, Lehrstuhl Informatik 2)
  • Thomas Mertens: Optimization of Model Checking by Large Block Encoding, Bachelor Thesis, RWTH Aachen University, 2014 (supervisor: Tim Lange, Lehrstuhl Informatik 2)
  • Christoph Matheja: Reconciling Decidability of Separation Logic Entailment and Graph Grammar Language Inclusion, Master Thesis, RWTH Aachen University, 2014 (co-supervisor: Christina Jansen, Lehrstuhl Informatik 2)
  • Rim Jnidi: Modelling and Analysing Security Properties of a Multi-Level File System, Master Thesis, RWTH Aachen University, 2014 (co-supervisor: Kevin van der Pol, Lehrstuhl Informatik 2)
  • David Laukamp: Efficient Generation of Multi-Terminal Binary Decision Diagrams for Probabilistic Model Checking, Bachelor Thesis, RWTH Aachen University, 2013 (supervisor: C. Dehnert, Lehrstuhl Informatik 2)
  • Samiro Discher: Graph-Based Interprocedural Analysis of Heap-Manipulating Programs, Bachelor Thesis, RWTH Aachen University, 2013 (supervisor: C. Jansen, Lehrstuhl Informatik 2)
  • Benjamin Kaminski: Analyzing the Communication Behaviour of LOOP+ω Programs, Master Thesis, RWTH Aachen University, 2013
  • Manuel Weiand: Efficient Generation of Small Critical Subsystems in Discrete-Time Markov Chains, Bachelor Thesis, RWTH Aachen University, 2013 (supervisor: C. Dehnert, Lehrstuhl Informatik 2)
  • Stephan Herold: Automatisierte Bewertung der Angemessenheit von Java-Code, Masterarbeit, RWTH Aachen University, 2013
  • David Clermont: Analyzing the Timed Behavior of SLIM Specifications, Diplomarbeit, RWTH Aachen University, 2013
  • Tim Lange: Code-Based Model Minimization for PLC Code Verification, Master Thesis, RWTH Aachen University, 2013 (co-supervisor: Dr. Neuhäußer, Siemens AG)
  • Christof Mroz: Formal Models for Diagnosability Analysis, Bachelor Thesis, RWTH Aachen University, 2013
  • Florian Göbe: Transformation von Separation-Logic-Prädikaten durch Hyperkantenersetzungsgrammatiken, Master Thesis, RWTH Aachen University, 2012 (supervisor: C. Jansen, Lehrstuhl Informatik 2)
  • Jens Katelaan: Type Theory, Certified Programming and Compiler Verification, Bachelor Thesis, RWTH Aachen University, 2012
  • Max Görtz: Deciding MSO over Languages of Hypergraphs, Bachelor Thesis, RWTH Aachen University, 2012 (supervisor: J. Heinen, Lehrstuhl Informatik 2)
  • Sebastian Staack: Optimierung von Sensorkonfigurationen zur Fehlerdiagnose in technischen Systemen, Diplomarbeit, RWTH Aachen University, 2012
  • Tobias Hoffmann: Model Checking Quantifizierter Linearer Temporaler Logik über Pointerprogrammen, Diplomarbeit, RWTH Aachen University, 2012 (supervisor: J. Heinen, Lehrstuhl Informatik 2)
  • Bernhard Ern: Model-Based Criticality Analysis by Impact Isolation, Master Thesis, RWTH Aachen University, 2012 (supervisor: V.Y. Nguyen, Lehrstuhl Informatik 2)
  • Gereon Kremer: Syntactic and Semantic Analysis of Hyperedge Replacement Grammars for Heap Abstraction, Bachelor Thesis, RWTH Aachen University, 2011 (supervisor: J. Heinen, Lehrstuhl Informatik 2)
  • Rafal Korzeniewski: Formal Approaches to System Diagnosability and Sensor Configuration Synthesis, Bachelor Thesis, RWTH Aachen University, 2011
  • Markus Bals: Incremental Greibach Normal Form, Diplomarbeit, RWTH Aachen University, 2011 (supervisor: C. Jansen, Lehrstuhl Informatik 2)
  • Johanna Nellen: Konfluenzanalyse und Vervollständigung von Graphersetzungssystemen, Diplomarbeit, RWTH Aachen University, 2010 (supervisor: C. Jansen, Lehrstuhl Informatik 2)
  • Jan Scherer: An Eclipse-Based Debugger for Embedded Systems Software, Diplomarbeit, RWTH Aachen University, 2010 (co-supervisor: Dr. Weber, Formal Methods and Tools Group, University of Twente)
  • Max Odenbrett: Explicit-State Model Checking of an Architectural Design Language using SPIN, Diplomarbeit, RWTH Aachen University, 2010
  • Christina Jansen: Konstruktion und Inferenz von Heapabstraktionsgrammatiken, Diplomarbeit, RWTH Aachen University, 2010
  • Ralf Grossmann: Heapabstraktion durch partielle Graphreduktion mittels Graphgrammatiken, Diplomarbeit, RWTH Aachen University, 2009
  • Mian Mohammad Junaid Tariq: An Agent-Based Simulation Environment for Large Scale Infrastructures of Heterogeneous Service-Based Devices, Master Thesis, RWTH Aachen University, 2008
  • Lars Helge Haß: Gleichungsbasierte Abstraktionen für Rewrite Theories, Diplomarbeit, RWTH Aachen University, 2007
  • Martin Neuhäußer: Abstraktion und Model Checking von Core Erlang-Programmen in Maude, Diplomarbeit, RWTH Aachen University, 2005
  • Paul Tawiah: Modelling Core Erlang in the Pi-Calculus: Translations and Correctness Proofs, Master Thesis, RWTH Aachen University, 2005
  • Jose Alberto Mejia Villar: Decision Algorithms for the Bisimulation Problem of Finite-State Processes, Master Thesis, RWTH Aachen University, 2005
  • Stefan Rieger: Analyse und Optimierung linearen Codes, Diplomarbeit, RWTH Aachen University, 2005
  • Chanchal Kumar Roy: Modelling Programming Languages for Concurrent and Distributed Systems in Specification Languages, Master Thesis, RWTH Aachen University, 2004
  • Stephan Küpper: Gleichungsbasierte Abstraktionen für Erlang-Programme, Diplomarbeit, RWTH Aachen University, 2003
  • Vazha Amiranashvili: A Rewriting Logic Formalization of Core Erlang Semantics, Master Thesis, RWTH Aachen University, 2002
  • Achim Müller: Syntaktische Transformationen natürlichsprachlicher Sätze – Baumtransformationen, Diplomarbeit, RWTH Aachen University, 1996
  • Frank Huch: Syntaktische Analyse natürlichsprachlicher Sätze – Fehleranalyse und Recovery, Diplomarbeit, RWTH Aachen University, 1996
  • Stefan Roßmanith: Kombination von LR-Parsing und paralleler Auswertung attributierter Grammatiken, Diplomarbeit, RWTH Aachen University, 1996
  • Olaf Chitil: Denotationelle und operationelle Semantiken für konstruktorbasierte funktionale Programmiersprachen erster Ordnung, Diplomarbeit, RWTH Aachen University, 1995
  • Michael Zenzes: Attributierte Grammatiken höherer Ordnung und Logikprogramme, Diplomarbeit, RWTH Aachen University, 1995
  • Marc Spielmann: Vergleich von primitiv rekursiven Funktionen höherer Ordnung mit mehrfach rekursiven Funktionen, Diplomarbeit, RWTH Aachen University, 1995
  • Ingo Krahn: Fehleranalyse und Recovery bei syntaktischen Transformationen natürlichsprachlicher Texte, Diplomarbeit, RWTH Aachen University, 1995
  • Jürgen Nelz: Die Berechnungsstärke attributierter Grammatiken höherer Ordnung, Diplomarbeit, RWTH Aachen University, 1995
  • Michael Mosler: Implementierung eines Parallelisierungsalgorithmus für imperative Programme, Diplomarbeit, RWTH Aachen University, 1994
  • Can Adam Albayrak: Vergleichende Gegenüberstellung der Parameterübergabemechanismen Call-by-name und Call-by-value im Rahmen funktionaler Programme, Diplomarbeit, RWTH Aachen University, 1993
  • Klaudia Bock: Erarbeitung eines objektorientierten Konzeptes zur Editierung statischer Eigenschaften und zur Spezifikation des dynamischen Verhaltens von Applikationsobjekten, Diplomarbeit, RWTH Aachen University, 1992