Thesis Projects

If you are interested in writing your master or bachelor thesis in the MOVES group, please contact Prof. Dr. Joost-Pieter Katoen, Prof. Dr. Thomas Noll, or the person indicated with the topics below.

Open topics

Open since Type Topic Supervisor
2021 August BSc/MSc Proving Termination of Probabilistic Recursive Programs via SMT-Solving (reserved) Tobias Winkler
2021 March MSc Generating invalid C-code using SMT solving Jana Berger
2020 December MSc Investigating Security-related Trees in Storm Shahid Khan
2020 October MSc Probabilistic Inference on Dynamic Bayesian Networks
 Bahare Salmani
2020 May MSc On ∞-Safety of Probabilistic Programs Mingshuai Chen
2020 April MSc Linux Kernel – Findings Bugs with Model Checking
 Jana Berger
2020 February BSc/MSc Metrics and Equivalences on formal Power Series for Probabilistic Program Analysis Lutz Klinkenberg
2020 February BSc/MSc Decomposing Probabilistic Program Semantics Computation using Stochastically Independence Lutz Klinkenberg
2020 February BSc/MSc Closed-form Operations on Probability Generating Functions  Lutz Klinkenberg

Current projects

Student Type Topic Supervisor
Laura Bamberger Bachelor’s Thesis Implementation of an LTL Model Checker for Probabilistic Push-Down Automata Tobias Winkler
Denis Kuksaus Master’s Thesis Verification of Multi-agent Markov Decision Processes
 Tim Quatmann
Leon Barth Bachelor’s Thesis Compositional Control-Flow Reduction for Probabilistic Model Checking Tobias Winkler
Denise Cassandra Fromme Master’s Thesis TBA Lutz Klinkenberg
Hermann Walth Master’s Thesis Marking boundaries of fault trees and architectural description languages Shahid Khan
Markus Miliats Bachelor’s Thesis Sensitivity Analysis for Dynamic Fault Trees Matthias Volk
Xaver Eugen Fink Bachelor’s Thesis Automatically generating and
benchmarking case studies for C-code model checking
 Philipp Berger
Patrick Arens Bachelor’s Thesis Extending and applying weakest-preexpectation to (disjoint) concurrent probabilistic progams Ira Fesefeldt
Mohamed Khalifa Master’s Thesis Extending a Static Termination Analysis for Heap-Manipulating Programs to Recursion Ira Fesefeldt
Domenic Quirl Master’s Thesis IDE-Ready Parsing of Compile-Time Dynamic Languages Thomas Noll
Fabian Gasser Bachelor’s Thesis Analysis of Concurrent Probabilistic Programs with Shared Variables Ira Fesefeldt, Thomas Noll

Award Winning Theses

Student Topic Award Supervisor
Christina Gehnen Automata-based Model Checking of Recursive Systems Preis der Fachgruppe Informatik der RWTH für eine herausragende Bachelorarbeit (2021) Tobias Winkler
Jan Svejda Interpretation-Based Violation Witness Validator. Master’s Thesis. DSA Industrial Award (2020) Philipp Berger
Florian Keßler On the Decidability of Entailment Checking in Quantitative Separation Logics. Bachelor’s Thesis. Preis der Fachgruppe Informatik der RWTH Aachen für die beste Bachelorarbeit (2020) Thomas Noll
Lea Hiendl Human-readable Scheduler Representation for Markov Decision Processes
 Berthold Vöcking Master Award (2018) Tim Quatmann
Clara Scherbaum Probability Generating Function Semantics for Probabilistic Programs. Bachelor’s Thesis. itestra innovation Award (2016)
 Benjamin Kaminski
Sebastian Junges Simplifying Dynamic Fault Trees by Graph Rewriting. Master’s Thesis.

Preis des Fakultätentags Informatik für die beste Masterarbeit (2015) 

Preis der Fachgruppe Informatik der RWTH Aachen für die beste Masterarbeit (2015)

 Joost-Pieter Katoen
Sergey Sazonov Property Preservation under Bisimulations on Markov Automata. Master’s Thesis. Preis der Fachgruppe Informatik der RWTH Aachen für die beste Masterarbeit (2014) Joost-Pieter Katoen
Jens Katelaan Type Theory, Certified Programming and Compiler Verification. Bachelor’s Thesis. Schönebornpreis (2013) Thomas Noll
Falak Sher Compositional Abstraction for Probabilistic Automata. Master’s Thesis. Microsoft Innovation Award (2010) Joost-Pieter Katoen

 

Past Projects

2021
DOI fulltext PDF [bibtex]
@masterthesis{LS2021,
title = {Learning probabilistic automata with SMT solving},
author = {Dario Veltri},
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, 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, Tim Quatmann. 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.
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{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, Jip Josephine Spel. 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, Matthias Volk, Shahid Khan. 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, Shahid Khan. A petri net semantics for boolean-logic driven markov processes, Master Thesis, RWTH Aachen University, 55 Seiten, 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},
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, 118 S., 2019.
2011
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},
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.
2020
Florian Keßler. On the Decidability of Entailment Checking in Quantitative Separation Logics. Bachelor Thesis at RWTH Aachen University, 2020.
Tobias Wirtz. Support for Java Libraries in the Attestor Shape Analysis Tool. Bachelor Thesis at RWTH Aachen University, 2020.
DownloadLinkFynn Mazurkiewicz. Parameter Synthesis for Continuous-Time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2020.
2019
DownloadLinkJan Švejda. Interpretation-Based Violation Witness Validator - A novel approach to validation. Master Thesis at RWTH Aachen University, 2019.
Sally Chau. Comparing Hierarchical and On-The-Fly Model Checking for Java Pointer Programs. Master Thesis at RWTH Aachen University, 2019.
DownloadLinkJohannes Schulte. Automated Detection and Completion of Confluence for Graph Grammars. Master Thesis at RWTH Aachen University, 2019.
DownloadLinkPaul Lambrich. Precise Long Run Averages for Markov Decision Processes. Bachelor Thesis at RWTH Aachen University, 2019.
Sebastian Bartsch. Systematic Design of Efficient Online Scanners. Bachelor Thesis at RWTH Aachen University, 2019.
DownloadLinkMirela Mileva. Minimising Mealy Machines with Dependent Inputs. Bachelor Thesis at RWTH Aachen University, 2019.
Hannah Mertens. Repairs in Dynamic Fault Trees: a Petri net semantics. Bachelor Thesis at RWTH Aachen University, 2019.
DownloadLinkCaroline Jabs. Expected Runtimes of Probabilistic Pointer Programs. Bachelor Thesis at RWTH Aachen University, 2019.
Sonja Skiba. Towards Completeness of a Proof Rule for Almost-Sure Termination. Bachelor Thesis at RWTH Aachen University, 2019.
David Herzkamp. Hardness of Probabilistic Termination with Nondeterminism. Bachelor Thesis at RWTH Aachen University, 2019.
Hannah Arndt. Randomized Meldable Heaps: A More Formal Proof of a Less Simple Probabilistic Data Structure. Master Thesis at RWTH Aachen University, 2019.
Philipp Schroer. Understanding Abstraction of Probabilistic Programs. Bachelor Thesis at RWTH Aachen University, 2019.
Lutz Klinkenberg. On Probability Generating Functions for Program Analysis. Master Thesis at RWTH Aachen University, 2019.
DownloadLinkLukas Westhofen. Verifying Automotive C Code using Modern Software Model Checkers. Master Thesis at RWTH Aachen University, 2019.
2018
DownloadLinkAlexander Bork. Analysing Dynamic Fault Trees by GSPNs. Bachelor Thesis at RWTH Aachen University, 2018.
Sabrina Kowarsch. Modeling and Analysis of a Spacecraft Mission. Master Thesis at RWTH Aachen University, 2018.
Fabian Schneider. A Unified Algebraic Shape Domain. Master Thesis at RWTH Aachen University, 2018.
DownloadLinkLea Hiendl. Human-readable Scheduler Representation for Markov Decision Processes. Master Thesis at RWTH Aachen University, 2018.
Felix Bier. From Forest Automata to Hyperedge Replacement Grammars and Back. Master Thesis at RWTH Aachen University, 2018.
2017
Sven Deserno. Probabilistic Model Checking for Markov Chain Families. Master Thesis at RWTH Aachen University, 2017.
Daniel Cloerkes. A Cyclic Proof System for Graph Grammar Inclusion. Bachelor Thesis at RWTH Aachen University, 2017.
Dustin Jungen. Repairs in Dynamic Fault Trees. Bachelor Thesis at RWTH Aachen University, 2017.
Michael Deutschen. Petri net semantics for Dynamic Fault Trees. Master Thesis at RWTH Aachen University, 2017.
DownloadLinkKevin Batz. Proof Rules for Expected Run-Times of Probabilistic Programs. Bachelor Thesis at RWTH Aachen University, 2017.
2016
Ronja Nocon. Pattern based analysis of monotonicity on Dynamic Fault Trees. Bachelor Thesis at RWTH Aachen University, 2016.
DownloadLinkThomas Mertens. Efficient reuse of learnt information for control-flow oriented IC3 algorithms. Master thesis at RWTH Aachen University, 2016.
DownloadLinkFrederick Prinz. Generalisation methods for control-flow oriented IC3 algorithms. Master thesis at RWTH Aachen University, 2016.
DownloadLinkTim Quatmann. Multi-Objective Model Checking of Markov Automata. Master Thesis at RWTH Aachen University, 2016.
Tom Janson. Accelerated Model Repair using Heuristic Analysis of Subsystems. Bachelor Thesis at RWTH Aachen University, 2016.
Isabelle Tülleners. Graph-based Heap Abstraction for Balanced Data Structures. Bachelor Thesis at RWTH Aachen University, 2016.
DownloadLinkHannah Arndt. Heap Abstraction Beyond Context-Freeness. Bachelor Thesis at RWTH Aachen University, 2016.
DownloadLinkHanna Franzen. Graph-Based Symbolic Execution for Pointer Programs with Data. Bachelor Thesis at RWTH Aachen University, 2016.
Simon Feiden. Extending Probability Generating Function Semantics to Negative Variable Valuations. at RWTH Aachen University, 2016.
Raoul Schaffranek. Modelling a Purely Functional Subset of EcmaScript2015. Bachelor Thesis at RWTH Aachen University, 2016.
Louis Wachtmeister. Analysing Cryptographically-Masked Information Flows Using Slicing. Bachelor Thesis at RWTH Aachen University, 2016.
David Korzeniewski. McMillan Prefixes for Stochastic Petri Nets. Master Thesis at RWTH Aachen University, 2016.
2015
DownloadLinkLukas Armborst. Generating Simulink Models from AADL system descriptions. Bachelor Thesis at RWTH Aachen University, 2015.
DownloadLinkMichael Beaumont. Efficient computation of weakest preconditions. Bachelor Thesis at RWTH Aachen University, 2015.
DownloadLinkSascha Müller. Evaluating control-flow based inductive model checking algorithms. Master Thesis at RWTH Aachen University, 2015.
DownloadLinkJustin Winkens. Loop Invariants in Probabilistic Programs. Bachelor Thesis at RWTH Aachen University, 2015.
Manuel Sascha Weiand. Checking Reachability Properties in Parametric MDPs. Master's Thesis at RWTH Aachen University, 2015.
Clara Scherbaum. Probability Generating Function Semantics for Probabilistic Programs. Bachelor Thesis at RWTH Aachen University, 2015.
LinkChristoph Welzel. Thread-Modular Analysis of Heap-Manipulating Programs. Bachelor Thesis at RWTH Aachen University, 2015.
DownloadLinkSascha Vincent Kurowski. Qualitative Model Checking of Markov Decision Processes on GPUs. Bachelor's Thesis at RWTH Aachen University, 2015.
DownloadLinkSebastian Junges. Simplifying Dynamic Fault Trees by Graph Rewriting. Master Thesis at RWTH Aachen University, 2015.
LinkJens Katelaan. Modular Analysis of Concurrent Pointer Programs. Master's Thesis at RWTH Aachen University, 2015.
DownloadLinkLukas Westhofen. On-the-fly Model Checking of Probabilistic Programs. Bachelor's Thesis at RWTH Aachen University, 2015.
2014
DownloadLinkThomas Mertens. Optimization of Model Checking by Large Block Encoding. Bachelor Thesis at RWTH Aachen University, 2014.
LinkLinkLisa von Büttner. Probabilistic Backward Bisimulation on Interactive Markov Chains. Master Thesis at RWTH Aachen University, 2014.
DownloadLinkFrederick Prinz. Symbolic Model Checking of Probabilistic Systems using Multi-Terminal Binary Decision Diagrams. Bachelor Thesis at RWTH Aachen University, 2014.
DownloadLinkPhilipp Florian. Efficiently Computing Poisson Probabilities for Model Checking Continuous-time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2014.
DownloadLinkPhilipp Berger. GPU-aided Model Checking of Markov Decision Processes. Bachelor Thesis at RWTH Aachen University, 2014.
DownloadLinkDimitri Bohlender. Accelerating Predicate Abstraction for Probabilistic Automata. Master Thesis at RWTH Aachen University, 2014.
DownloadLinkTim Quatmann. Counterexamples for Expected Rewards on Discrete-time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2014.
DownloadLinkChristoph Matheja. Reconciling Decidability of Separation Logic Entailment and Graph Grammar Language Inclusion. Master Thesis at RWTH Aachen University, 2014.
DownloadLinkDavid Korzeniewski. CEGAR for Computing High-Level Counterexamples for Probabilistic Systems. Bachelor Thesis at RWTH Aachen University, 2014.
Rim Jnidi. Modelling and Analysing Security Properties of a Multi-Level File System. Master Thesis at RWTH Aachen University, 2014.
LinkLinkChristopher Kugler. A polytope library for the reachability analysis of hybrid systems. Master thesis at RWTH Aachen University, 2014.
LinkLinkDustin Hütter. SMT solving for linear integer arithmetic. Bachelor thesis at RWTH Aachen University, 2014.
LinkLinkMaik Glatki. A zonotope library for hybrid systems reachability analysis. Bachelor thesis at RWTH Aachen University, 2014.
LinkLinkKai Driessen. Modular verification for PLC controlled hybrid systems. Master thesis at RWTH Aachen University, 2014.
2013
DownloadLinkSergey Sazonov. Property Preservation under Bisimulations on Markov Automata. Master Thesis at RWTH Aachen University, 2013.
Yannis Samiro Discher. Graph-Based Interprocedural Analysis of Heap-Manipulating Programs. Bachelor Thesis at RWTH Aachen University, 2013.
DownloadLinkBenjamin Lucien Kaminski. Analyzing the Communication Behavior of LOOP+Omega Programs. Master Thesis at RWTH Aachen University, 2013.
DownloadLinkGereon Kremer. Isolating Real Roots Using Adaptable-Precision Interval Arithmetic. at RWTH Aachen University, 2013.
Tim Lange. Code-Based Model Minimization for PLC Code Verification. Master Thesis at RWTH Aachen University, 2013.
Christof Mroz. Formal Models for Diagnosability Analysis. Bachelor Thesis at RWTH Aachen University, 2013.
David Clermont. Analyzing the Timed Behavior of SLIM Specifications. Diplomarbeit at RWTH Aachen University, 2013.
DownloadLinkStefan Schupp. Interval Constraint Propagation in SMT Compliant Decision Procedures. at RWTH Aachen University, 2013.
Andreas Vorpahl. Compositional counterexamples for MDPs. Master thesis at RWTH Aachen University, 2013.
Marian van de Veire. Minimal critical subsystems for probabilistic models with nondeterminism. Diploma thesis at RWTH Aachen University, 2013.
LinkLinkHenrik Schmitz. Parallel user-defined strategies for QFNRA. Diploma thesis at RWTH Aachen University, 2013.
LinkLinkThomas Osterland. Memory- and time-related action qualifiers in HSFCs. Bachelor thesis at RWTH Aachen University, 2013.
LinkLinkAmith Belur Nagabushana. Minimal critical subsystems for PCTL. Master thesis at RWTH Aachen University, 2013.
LinkLinkGeorg Jenneßen. Solar tower optimisation with genetic algorithms. Diploma thesis at RWTH Aachen University, 2013.
LinkLinkKim Maren Haps. Datatypes and tools for the analysis of hybrid systems. Bachelor thesis at RWTH Aachen University, 2013.
LinkLinkMatthias Ewert. Modellierung des Radialverdichters eines PKW-Abgasturboladers. Master thesis at RWTH Aachen University, 2013.
2012
DownloadLinkHussein Hamid Baagil. Quantitative Message Sequence Graphs. Master Thesis at RWTH Aachen University, 2012.
DownloadLinkFlorian Göbe. Transformation von Separation Logic Prädikaten durch Hyperkantenersetzungsgrammatiken. at RWTH Aachen, 2012.
Bart Postma. Modeling and Analysis of Dependable Space Systems. at University of Twente, 2012.
DownloadLinkMax Görtz. Deciding MSO over Languages of Hypergraphs. Bachelorthesis at RWTH Aachen University, 2012.
DownloadLinkAlexander Dominik Weinert. Inferring Heap Abstraction Grammars. Bachelor Thesis at RWTH Aachen University, 2012.
DownloadLinkTobias Hoffmann. Model Checking Quantifizierter Linearer Temporaler Logik über Pointerprogrammen. Diplomarbeit at RWTH Aachen University, 2012.
DownloadLinkBernhard Ern. Model-Based Criticality Analysis by Impact Isolation. at RWTH Aachen University, 2012.
Jens Katelaan. Type Theory, Certified Programming and Compiler Verification. Bachelor Thesis at RWTH Aachen University, 2012.
Sebastian Staack. Optimierung von Sensorkonfigurationen zur Fehlerdiagnose in technischen Systemen. Diplomarbeit at RWTH Aachen University, 2012.
Christoph Worreschk. Weighted Lumpability on Markov Chains. Bachelor Thesis at RWTH Aachen University, 2012.
Maik Scheffler. Hierarchical counterexamples for DTMCs – Case studies. Diploma thesis at RWTH Aachen University, 2012.
Canan Kasaci. Model-based resource monitoring and optimization. Master thesis at RWTH Aachen University, 2012.
LinkLinkJoachim Redies. An extension of the GiNaCRA library for the cylindrical algebraic decomposition. Bachelor thesis at RWTH Aachen Universtiy, 2012.
LinkLinkMatthias Volk. Verification and synthesis for parametric Markov chains. Bachelor thesis at RWTH Aachen University, 2012.
LinkLinkSebastian Junges. On Gröbner bases in SMT-compliant decision procedures. Bachelor thesis at RWTH Aachen University, 2012.
Dennis Scully. Preprocessing for solving non-linear real-arithmetic formulas. Bachelor thesis at RWTH Aachen University, 2012.
LinkLinkKai Driessen. Counterexample-guided abstraction refinement for hybrid SFC verification. Bachelor thesis at RWTH Aachen University, 2012.
LinkLinkAlin Ionascu. Modeling and controler synthesis of hybrid propulsion systems using artificial intelligence. Master thesis at RWTH Aachen University, 2012.
2011
DownloadLinkHenrik Barthels. Automata-Based Detection of Hypergraph Embeddings. Bachelorarbeit at RWTH Aachen University , 2011.
DownloadLinkGereon Kremer. Syntaktische und semantische Analyse von Hyperkantenersetzungsgrammatiken zur Heapabstraktion. Bachelors Thesis at RWTH Aachen University, 2011.
DownloadLinkMarkus Bals. Incremental Greibach Normal Form. Diploma Thesis at RWTH Aachen University, 2011.
DownloadLinkChristian Dehnert. Symbolic Bisimulation Minimization of Markov Models. Diplomarbeit at RWTH Aachen University, 2011.
DownloadLinkLisa von Büttner. Stutter Simulation Minimisation. Bachelorarbeit at RWTH Aachen University, 2011.
DownloadLinkFlorian Corzilius. Virtual Substitution in SMT Solving. Diploma thesis at RWTH Aachen, 2011.
DownloadLinkHao Wu. Semantics and Analysis of Scenario-Aware Dataflow Specifications. Diploma Thesis at RWTH Aachen University, 2011.
DownloadLinkHauke Schaper. Translation of Sequential Function Charts to Transition Systems. Bachelorarbeit at RWTH Aachen University, 2011.
DownloadLinkSilvio de Carolis. Zuverlässigkeitsanalyse dynamischer Fehlerbäume. at RWTH Aachen University, 2011.
Rafal Korzeniewski. Formal Approaches to System Diagnosability and Sensor Configuration Synthesis. at RWTH Aachen University, 2011.
2010
DownloadLinkFriedrich Gretz. Invariant Generation for Linear Probabilistic Programs. Diplomarbeit at RWTH Aachen University, 2010.
Johanna Nellen. Konfluenzanalyse und Vervollständigung von Graphersetzungssystemen. Diplomarbeit at RWTH Aachen University, 2010.
Frank Fiedler. TripleT: Ein Werkzeug zum Echtzeittesten von reaktiven Systemen. Diplomarbeit at RWTH Aachen University, 2010.
Jan Scherer. An Eclipse-based Debugger for Embedded Systems Software. Diplomarbeit at RWTH Aachen University/University of Twente, 2010.
DownloadLinkFalak Sher. Compositional Abstraction for Probabilistic Automata. Master Thesis at RWTH Aachen University, 2010.
LinkLinkMaximilian R. Odenbrett. Explicit-State Model Checking of an Architectural Design Language using SPIN. Diplomarbeit at RWTH Aachen University, 2010.
Mark Bretsch. Automatic Code-Generation for a High-Level Virtual Platform from Process Network. Diplomarbeit at RWTH Aachen University, 2010.
DownloadLinkChristina Jansen. Entwicklung eines Inferenzalgorithmus für Hyperkantenersetzungsgrammatiken. Diplomarbeit at RWTH Aachen University, 2010.
Dennis Guck. Analysis and scheduler synthesis of time-bounded reachability in continuous-time Markov decision processes. Bachelorarbeit at RWTH Aachen University, 2010.
DownloadLinkStefan Herting. An Equivalence and Minimization Algorithm for CTMCs. Diplomarbeit at RWTH Aachen University, 2010.
Malte Kampschulte. Evaluation of radio models for the analysis of a gossiping MAC protocol. Bachelor Thesis at RWTH Aachen University, 2010.
2009
DownloadLinkSabrina von Styp. Towards a Testing Theory for Timed and Symbolic Systems. Diplomarbeit at RWTH Aachen University, 2009.
DownloadLinkChitra Hapsari Ayuningtyas. Probabilistic Message Sequence Charts. at RWTH Aachen University/University of Trento, 2009.
Ulrich Loup. Decision Problems over the Domain of the Real Numbers. Diploma thesis at RWTH Aachen, 2009.
Ralf Grossmann. Heapabstraktion durch partielle Graphreduktion mittels Graphgrammatiken . Diplomarbeit at Faculty of Mathematics, Computer Sciences and Natural Sciences,RWTH Aachen University , 2009.
Silvio de Carolis. Modeling and Analysis of Leader-Election Protocols in Ad-Hoc Networks . Bachelor Thesis at RWTH Aachen University, 2009.
LinkLinkPascal Richter. Simulation und Auslegungsoptimierung solarthermischer Kraftwerke unter Einsatz evolutionärer Algorithmen und neuronaler Netze. Diploma thesis at RWTH Aachen University, 2009.
2008
Berteun Damman. Representing PCTL Counterexamples. Master Thesis at University of Twente, The Netherlands, 2008.
Mian Mohammad Junaid Tariq. An Agent-Based Simulation Environment for Large Scale Infrastructures of Heterogeneous Service-Based Devices. Master Thesis at RWTH Aachen University, 2008.
André Kolbe. Untersuchung der Anwendbarkeit des Timed Testing in der Eisenbahn-Signaltechnik. Diplomarbeit at RWTH Aachen University, 2008.
DownloadLinkNils Jansen. Automaton-definable Tree Relations with Cardinality Constraints. Diploma Thesis at RWTH Aachen University, 2008.
2007
Lars Helge Haß. Gleichungsbasierte Abstraktionen für Rewrite Theories. Diplomarbeit at RWTH Aachen University, 2007.
Alexandru Mereacre. Modeling and Verification of Time-Inhomogeneous Markov Chains. Master Thesis at RWTH Aachen/University of Trento, 2007.
DownloadLinkTim Kemna. Bisimulation Minimization in Probabilistic Model Checking. Master Thesis at University of Twente, 2007.
DownloadLinkMarcel Oldenkamp. Experimental Comparison of Probabilistic Model Checkers. Master Thesis at University of Twente, 2007.
2006
DownloadLinkDaniel Willems. Abstraktion zeitstetiger Markov-Ketten. Diploma Thesis at Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University, 2006.
DownloadLinkGustavo Quirós. Static Byte-Code Analysis for State Space Reduction. Master Thesis at RWTH Aachen University, 2006.
2005
DownloadLinkStefan Rieger. Analyse und Optimierung linearen Codes. Diploma Thesis at Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University, 2005.
Carsten Kern. MSCan - Ein Tool zur Analyse von Message Sequence Charts. Diploma Thesis at Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University, 2005.
Martin R. Neuhäußer. Abstraktion und Model Checking von Core Erlang-Programmen in Maude. Diplomarbeit at RWTH Aachen University, 2005.
DownloadLinkJasper Berendsen. Reachability in Weighted Probabilistic Timed Automata. Master Thesis at University of Twente, 2005.