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 at i2.informatik.rwth-aachen.de (kindly include your transcript of records).

Award Winning Theses

StudentTopicAwardSupervisor
Tom BiskupInvariant-based Strategy Synthesis for Nondeterministic Probabilistic ProgramsBerthold Vöcking Master Award (2023)Kevin Batz
Tobias Winkler
Marvin JansenDecidability and Complexity of Entailment Checking in Quantitative Separation LogicPreis der Fachgruppe Informatik der RWTH für eine herausragende Masterarbeit (2021)Kevin Batz
Christina GehnenAutomata-based Model Checking of Recursive SystemsPreis der Fachgruppe Informatik der RWTH für eine herausragende Bachelorarbeit (2021)Tobias Winkler
Jan SvejdaInterpretation-Based Violation Witness Validator. Master’s Thesis.DSA Industrial Award (2020)Jana Berger
Florian KeßlerOn 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 HiendlHuman-readable Scheduler Representation for Markov Decision Processes
Berthold Vöcking Master Award (2018)Tim Quatmann
Clara ScherbaumProbability Generating Function Semantics for Probabilistic Programs. Bachelor’s Thesis.itestra innovation Award (2016)
Benjamin Kaminski
Sebastian JungesSimplifying 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 SazonovProperty 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 KatelaanType Theory, Certified Programming and Compiler Verification. Bachelor’s Thesis.Schönebornpreis (2013)Thomas Noll
Falak SherCompositional Abstraction for Probabilistic Automata. Master’s Thesis.Microsoft Innovation Award (2010)Joost-Pieter Katoen

Past Projects

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{C2024,
title = {Complexity and decidability of multi-objective stochastic games},
author = {Tobias Winkler},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02592},
url = { https://publications.rwth-aachen.de/record/980848},
}×
[issue] 		Tobias Winkler. Complexity and decidability of multi-objective stochastic games, Master 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{PS2024,
title = {Proving termination of probabilistic recursive programs via SMT-solving},
author = {Leo Mommers},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource : Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-02602},
url = { https://publications.rwth-aachen.de/record/980858},
}×
[issue] 		Leo Mommers. Proving termination of probabilistic recursive programs via SMT-solving, 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.
DOI fulltext PDF [bibtex]
@masterthesis{M2024,
title = {Model checking pPDA vs unambiguous automata},
author = {Anastasiia Petrova},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-06745},
url = { https://publications.rwth-aachen.de/record/989355},
}×
[issue] 		Anastasiia Petrova. Model checking pPDA vs unambiguous automata, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{MBN2024,
title = {Most probable explanations in Bayesian Networks via weighted programming},
author = {Dinis Vitorino},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Bachelor Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-06746},
url = { https://publications.rwth-aachen.de/record/989356},
}×
[issue] 		Dinis Vitorino. Most probable explanations in Bayesian Networks via weighted programming, Bachelor Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{SJ2024,
title = {Semantics-preserving transformation of Java source code},
author = {Frederik Heigold},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/991802},
}×
[issue] 		Frederik Heigold. Semantics-preserving transformation of Java source code, Bachelor Thesis, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{O2024,
title = {Optimized routing for shuttling-based quantum processing architectures},
author = {Roy Hermanns},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/991804},
}×
[issue] 		Roy Hermanns. Optimized routing for shuttling-based quantum processing architectures, Master Thesis, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{H2024,
title = {Heuristic synthesis of spare parts inventories using dynamic fault trees},
author = {Jakob van Sprang},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/991805},
}×
[issue] 		Jakob van Sprang. Heuristic synthesis of spare parts inventories using dynamic fault trees, Bachelor Thesis, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{IGHPS2024,
title = {Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm},
author = {Sven Büge},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/992674},
}×
[issue] 		Sven Büge. Implementing Goal-HSVI for POMDPs in the probabilistic model checker Storm, Bachelor Thesis, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{E2024,
title = {Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs},
author = {Patrick Nossol},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-09539},
url = { https://publications.rwth-aachen.de/record/994779},
}×
[issue] 		Patrick Nossol. Entailments in quantitative separation logic with recursive definitions: constructing cyclyc proofs, Master Thesis, RWTH Aachen University, 1 Online-Ressource: Illustrationen, RWTH Aachen University, 2024.
[bibtex]
@masterthesis{D2024,
title = {Distributional invariants for probabilistic programs},
author = {Daniel Zilken},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2024},
url = { https://publications.rwth-aachen.de/record/995438},
}×
[issue] 		Daniel Zilken. Distributional invariants for probabilistic programs, Master Thesis, RWTH Aachen University, 2024.
DOI fulltext PDF [bibtex]
@masterthesis{A2024,
title = {A deductive verifier for probabilistic programs},
author = {Philipp Schroer},
publisher = {RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {1 Online-Ressource: Illustrationen},
type = {Master Thesis},
year = {2024},
doi = {10.18154/RWTH-2024-11340},
url = { https://publications.rwth-aachen.de/record/998370},
}×
[issue] 		Philipp Schroer. A deductive verifier for probabilistic programs, Master 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{C2022,
title = {Comparison of heuristics for branching in neural network verification},
author = {Jonas Seidel},
institution = {RWTH Aachen University},
pages = {75 Seiten : Illustrationen},
type = {Bachelor Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/985671},
}×
[issue] 		Jonas Seidel. Comparison of heuristics for branching in neural network verification, Bachelor Thesis, RWTH Aachen University, 75 Seiten : Illustrationen, 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.
[bibtex]
@masterthesis{A2022,
title = {Automatic verification of loop invariants in weighted programs},
author = {Ben Sturgis},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/989357},
}×
[issue] 		Ben Sturgis. Automatic verification of loop invariants in weighted programs, Bachelor Thesis, RWTH Aachen University, 2022.
[bibtex]
@masterthesis{I2022,
title = {Inference in discrete probabilistic programs using probability generating functions},
author = {Christian Blumenthal},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/989358},
}×
[issue] 		Christian Blumenthal. Inference in discrete probabilistic programs using probability generating functions, Master Thesis, RWTH Aachen University, 2022.
[bibtex]
@masterthesis{IL2022,
title = {Implementation of an LTL model checker for probabilistic pushdown automata},
author = {Laura Bamberger},
institution = {RWTH Aachen University},
type = {Bachelor Thesis},
year = {2022},
url = { https://publications.rwth-aachen.de/record/989359},
}×
[issue] 		Laura Bamberger. Implementation of an LTL model checker for probabilistic pushdown automata, Bachelor 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.
[bibtex]
@masterthesis{UP2021,
title = {Underapproximations for indefinite-horizon POMDPS},
author = {Alexander Nikolai Bork},
institution = {RWTH Aachen University},
type = {Master Thesis},
year = {2021},
url = { https://publications.rwth-aachen.de/record/972076},
}×
[issue] 		Alexander Nikolai Bork. Underapproximations for indefinite-horizon POMDPS, Master Thesis, RWTH Aachen University, 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.
[bibtex]
@masterthesis{P2020,
title = {Parameter synthesis in probabilistic timed automata},
author = {Bram Kohlen},
institution = {RWTH Aachen University},
pages = {91 Seiten},
type = {Master Thesis},
year = {2020},
url = { https://publications.rwth-aachen.de/record/811856},
}×
[issue] 		Bram Kohlen. Parameter synthesis in probabilistic timed automata, Master Thesis, RWTH Aachen University, 91 Seiten, 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.
2011
DOI fulltext PDF [bibtex]
@masterthesis{S2011,
title = {Static byte-code analysis for state space reduction},
author = {Gustavo Quirós Araya},
publisher = {Publikationsserver der RWTH Aachen University},
institution = {RWTH Aachen University},
pages = {VIII, 101 S.},
type = {Master Thesis},
year = {2011},
doi = {10.18154/RWTH-CONV-144790},
url = { https://publications.rwth-aachen.de/record/229985},
}×
[issue] 		Gustavo Quirós Araya. Static byte-code analysis for state space reduction, Master Thesis, RWTH Aachen University, VIII, 101 S., Publikationsserver der RWTH Aachen University, 2011.