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. |
  | Fynn Mazurkiewicz. Parameter Synthesis for Continuous-Time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2020. |
2019 |
  | Jan Š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. |
  | Johannes Schulte. Automated Detection and Completion of Confluence for Graph Grammars. Master Thesis at RWTH Aachen University, 2019. |
  | Paul 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. |
  | Mirela 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. |
  | Caroline 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. |
  | Lukas Westhofen. Verifying Automotive C Code using Modern Software Model Checkers. Master Thesis at RWTH Aachen University, 2019. |
2018 |
  | Alexander 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. |
  | Lea 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. |
  | Kevin 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. |
  | Thomas Mertens. Efficient reuse of learnt information for control-flow oriented IC3 algorithms. Master thesis at RWTH Aachen University, 2016. |
  | Frederick Prinz. Generalisation methods for control-flow oriented IC3 algorithms. Master thesis at RWTH Aachen University, 2016. |
  | Tim 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. |
  | Hannah Arndt. Heap Abstraction Beyond Context-Freeness. Bachelor Thesis at RWTH Aachen University, 2016. |
  | Hanna 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 |
  | Lukas Armborst. Generating Simulink Models from AADL system descriptions. Bachelor Thesis at RWTH Aachen University, 2015. |
  | Michael Beaumont. Efficient computation of weakest preconditions. Bachelor Thesis at RWTH Aachen University, 2015. |
  | Sascha Müller. Evaluating control-flow based inductive model checking algorithms. Master Thesis at RWTH Aachen University, 2015. |
  | Justin 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. |
 | Christoph Welzel. Thread-Modular Analysis of Heap-Manipulating Programs. Bachelor Thesis at RWTH Aachen University, 2015. |
  | Sascha Vincent Kurowski. Qualitative Model Checking of Markov Decision Processes on GPUs. Bachelor's Thesis at RWTH Aachen University, 2015. |
  | Sebastian Junges. Simplifying Dynamic Fault Trees by Graph Rewriting. Master Thesis at RWTH Aachen University, 2015. |
 | Jens Katelaan. Modular Analysis of Concurrent Pointer Programs. Master's Thesis at RWTH Aachen University, 2015. |
  | Lukas Westhofen. On-the-fly Model Checking of Probabilistic Programs. Bachelor's Thesis at RWTH Aachen University, 2015. |
2014 |
  | Thomas Mertens. Optimization of Model Checking by Large Block Encoding. Bachelor Thesis at RWTH Aachen University, 2014. |
  | Lisa von Büttner. Probabilistic Backward Bisimulation on Interactive Markov Chains. Master Thesis at RWTH Aachen University, 2014. |
  | Frederick Prinz. Symbolic Model Checking of Probabilistic Systems using Multi-Terminal Binary Decision Diagrams. Bachelor Thesis at RWTH Aachen University, 2014. |
  | Philipp Florian. Efficiently Computing Poisson Probabilities for Model Checking Continuous-time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2014. |
  | Philipp Berger. GPU-aided Model Checking of Markov Decision Processes. Bachelor Thesis at RWTH Aachen University, 2014. |
  | Dimitri Bohlender. Accelerating Predicate Abstraction for Probabilistic Automata. Master Thesis at RWTH Aachen University, 2014. |
  | Tim Quatmann. Counterexamples for Expected Rewards on Discrete-time Markov Chains. Bachelor Thesis at RWTH Aachen University, 2014. |
  | Christoph Matheja. Reconciling Decidability of Separation Logic Entailment and Graph Grammar Language Inclusion. Master Thesis at RWTH Aachen University, 2014. |
  | David 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. |
  | Christopher Kugler. A polytope library for the reachability analysis of hybrid systems. Master thesis at RWTH Aachen University, 2014. |
  | Dustin Hütter. SMT solving for linear integer arithmetic. Bachelor thesis at RWTH Aachen University, 2014. |
  | Maik Glatki. A zonotope library for hybrid systems reachability analysis. Bachelor thesis at RWTH Aachen University, 2014. |
  | Kai Driessen. Modular verification for PLC controlled hybrid systems. Master thesis at RWTH Aachen University, 2014. |
2013 |
  | Sergey 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. |
  | Benjamin Lucien Kaminski. Analyzing the Communication Behavior of LOOP+Omega Programs. Master Thesis at RWTH Aachen University, 2013. |
  | Gereon 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. |
  | Stefan 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. |
  | Henrik Schmitz. Parallel user-defined strategies for QFNRA. Diploma thesis at RWTH Aachen University, 2013. |
  | Thomas Osterland. Memory- and time-related action qualifiers in HSFCs. Bachelor thesis at RWTH Aachen University, 2013. |
  | Amith Belur Nagabushana. Minimal critical subsystems for PCTL. Master thesis at RWTH Aachen University, 2013. |
  | Georg Jenneßen. Solar tower optimisation with genetic algorithms. Diploma thesis at RWTH Aachen University, 2013. |
  | Kim Maren Haps. Datatypes and tools for the analysis of hybrid systems. Bachelor thesis at RWTH Aachen University, 2013. |
  | Matthias Ewert. Modellierung des Radialverdichters eines PKW-Abgasturboladers. Master thesis at RWTH Aachen University, 2013. |
2012 |
  | Hussein Hamid Baagil. Quantitative Message Sequence Graphs. Master Thesis at RWTH Aachen University, 2012. |
  | Florian 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. |
  | Max Görtz. Deciding MSO over Languages of Hypergraphs. Bachelorthesis at RWTH Aachen University, 2012. |
  | Alexander Dominik Weinert. Inferring Heap Abstraction Grammars. Bachelor Thesis at RWTH Aachen University, 2012. |
  | Tobias Hoffmann. Model Checking Quantifizierter Linearer Temporaler Logik über Pointerprogrammen. Diplomarbeit at RWTH Aachen University, 2012. |
  | Bernhard 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. |
  | Joachim Redies. An extension of the GiNaCRA library for the cylindrical algebraic decomposition. Bachelor thesis at RWTH Aachen Universtiy, 2012. |
  | Matthias Volk. Verification and synthesis for parametric Markov chains. Bachelor thesis at RWTH Aachen University, 2012. |
  | Sebastian 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. |
  | Kai Driessen. Counterexample-guided abstraction refinement for hybrid SFC verification. Bachelor thesis at RWTH Aachen University, 2012. |
  | Alin Ionascu. Modeling and controler synthesis of hybrid propulsion systems using artificial intelligence. Master thesis at RWTH Aachen University, 2012. |
2011 |
  | Henrik Barthels. Automata-Based Detection of Hypergraph Embeddings. Bachelorarbeit at RWTH Aachen University , 2011. |
  | Gereon Kremer. Syntaktische und semantische Analyse von Hyperkantenersetzungsgrammatiken zur Heapabstraktion. Bachelors Thesis at RWTH Aachen University, 2011. |
  | Markus Bals. Incremental Greibach Normal Form. Diploma Thesis at RWTH Aachen University, 2011. |
  | Christian Dehnert. Symbolic Bisimulation Minimization of Markov Models. Diplomarbeit at RWTH Aachen University, 2011. |
  | Lisa von Büttner. Stutter Simulation Minimisation. Bachelorarbeit at RWTH Aachen University, 2011. |
  | Florian Corzilius. Virtual Substitution in SMT Solving. Diploma thesis at RWTH Aachen, 2011. |
  | Hao Wu. Semantics and Analysis of Scenario-Aware Dataflow Specifications. Diploma Thesis at RWTH Aachen University, 2011. |
  | Hauke Schaper. Translation of Sequential Function Charts to Transition Systems. Bachelorarbeit at RWTH Aachen University, 2011. |
  | Silvio 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 |
  | Friedrich 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. |
  | Falak Sher. Compositional Abstraction for Probabilistic Automata. Master Thesis at RWTH Aachen University, 2010. |
  | Maximilian 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. |
  | Christina 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. |
  | Stefan 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 |
  | Sabrina von Styp. Towards a Testing Theory for Timed and Symbolic Systems. Diplomarbeit at RWTH Aachen University, 2009. |
  | Chitra 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. |
  | Pascal 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. |
  | Nils 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. |
  | Tim Kemna. Bisimulation Minimization in Probabilistic Model Checking. Master Thesis at University of Twente, 2007. |
  | Marcel Oldenkamp. Experimental Comparison of Probabilistic Model Checkers. Master Thesis at University of Twente, 2007. |
2006 |
  | Daniel Willems. Abstraktion zeitstetiger Markov-Ketten. Diploma Thesis at Faculty of Mathematics, Computer Sciences and Natural Sciences, RWTH Aachen University, 2006. |
  | Gustavo Quirós. Static Byte-Code Analysis for State Space Reduction. Master Thesis at RWTH Aachen University, 2006. |
2005 |
  | Stefan 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. |
  | Jasper Berendsen. Reachability in Weighted Probabilistic Timed Automata. Master Thesis at University of Twente, 2005. |