Theses (Co-)Supervised by Thomas Noll

First Reviewer/Supervisor

  • Sally Chau: Comparing Hierarchical and On-The-Fly Model Checking for Java Pointer Programs, Master Thesis, RWTH Aachen University (ongoing; supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Mirela Mileva: Minimising Mealy Machines with Dependent Inputs, Bachelor Thesis, RWTH Aachen University (ongoing)
  • Johannes Schultz: Automated Detection and Completion of Confluence for Graph Grammars, Master Thesis, RWTH Aachen University (ongoing; supervisor: Christoph Matheja, Lehrstuhl Informatik 2)
  • Philipp Schroer: Understanding Abstraction of Probabilistic Programs, Bachelor Thesis, RWTH Aachen University (ongoing; 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

Second Reviewer:

  • Yi Yang:  Towards a Verification Environment for Communication Controllers in Vehicles, Master Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Rumpe, Lehrstuhl Informatik 3)
  • Lutz Klingenberg:  On Probability Generating Functions for Program Analysis, Master Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • Marta Grobelna:  Integration of Hybrid Systems Verification in Matlab, Master Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Abraham, Theory of Hybrid Systems research group)
  • Dennis Ledwon:  White-Box Test Generation According to Multiple Coverage Criteria using Model Checking, Master Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Niklas Kotowski:  Application of Formal Methods in Autonomous Vehicle Control, Master Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Abraham, Theory of Hybrid Systems research group)
  • Sonja Skiba: Towards Completeness of a Proof Rule for Almost-Sure Termination, Bachelor Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • Marwa Maghnie: Simulation and Layout Optimization of Offshore Wind Farms, Master Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Abraham, Theory of Hybrid Systems research group)
  • Jiong Fu: Automatic Generation of Non-Termination Witnesses for C Programs, Master Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Giesl, LuFG Informatik 2)
  • Tim Bolender: Evaluating Action Languages in Architecture Modelling, Bachelor Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Rumpe, Lehrstuhl Informatik 3)
  • Rafael Zähl: Symbolic Execution of Arbitrary LLVM Programs, Bachelor Thesis, RWTH Aachen University (ongoing; supervisor: Prof. Wehrle, Lehrstuhl Informatik 4)
  • Kevin Batz: IC3 for Probabilistic Systems, Master Thesis, RWTH Aachen University, 2019 (supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • Julian Düstersiek: Uncertainty Quantification and Multi-Objective Optimization of Wind Farms, Bachelor Thesis, RWTH Aachen University, 2019 (supervisor: Prof. Abraham, Theory of Hybrid Systems research group)
  • Janik-Vasily Benzin:  A Generic Framework Enhanced with Services for the Verification of Distributed Systems, Bachelor Thesis, RWTH Aachen University, 2019 (supervisor: Prof. Rumpe, Lehrstuhl Informatik 3)
  • Lyndmila Vatskicheva: Using Simulation to Improve the Precision of Hybrid Systems Reachability Analysis, Bachelor Thesis, RWTH Aachen University, 2019 (supervisor: Prof. Abraham, Theory of Hybrid Systems research group)
  • Pascal Siewert: Erweiterung einer generischen, zeit-synchronen Theorie für die Verifikation verteilter Systeme, Bachelor Thesis, RWTH Aachen University, 2019 (supervisor: Prof. Rumpe, Lehrstuhl Informatik 3)
  • Philipp Hochmann: Lexical Analysis of Controlled Languages and the Development of a Tool for Input Support, Bachelor Thesis, RWTH Aachen University, 2019 (supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Dmitry Manuilov: Ein generisches Verifikations-Backend für Unterspezifikation in verteilten Systemen, Master Thesis, RWTH Aachen University, 2019 (supervisor: Deni Raco, Lehrstuhl Informatik 3)
  • Max Hofmann: Automated Function Equivalence Analysis, Bachelor Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Wehrle, Lehrstuhl Informatik 4)
  • David Duong: Ein generisches, kompositionales Verifikations-Framework für (nicht-)deterministische, zustandsbasierte Component&Connector Modelle, Master Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Rumpe, Lehrstuhl Informatik 3)
  • Timon Noethlichs:  Symbolic Distributed Execution of Socket-Based Systems, Bachelor Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Wehrle, Lehrstuhl Informatik 4)
  • Maximilian Winck:  Code Optimization for Network Function Chains, Bachelor Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Wehrle, Lehrstuhl Informatik 4)
  • Maximilian Hänel: Verwendbarkeit von Grammatikextraktion in Java, um sichere Parseralternativen anzubieten, Bachelor Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Rumpe, Lehrstuhl Informatik 3)
  • Filip Vukelic: Policy Iteration with Octagons for Static Analysis of PLC Programs, Bachelor Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Alexander Bork: Analysing Dynamic Fault Trees by GSPNs, Bachelor Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • Inokentiy Babushkin: Recording Symbolic Constraints Using LLVM IR Instrumentation, Bachelor Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Wehrle, Lehrstuhl Informatik 4)
  • Thies Strothmann: Automated Complexity Analysis of Recursive Java Programs, Master Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Justin Winkens: Context-Dependent Reachability Analysis for Hybrid Automata, Master Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Abraham, Theory of Hybrid Systems research group)
  • Stefan Dollase: Beyond Field Sensitivity: Modular Heap Shape Analysis for Java Programs, Master Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Johannes Przybilla: Automated Testing of Software Containing Externally Triggered Event Handlers, Bachelor Thesis, RWTH Aachen University, 2018 (supervisor: Daniel Schemmel, Felix Rath, Lehrstuhl Informatik 4)
  • Sabrina Kielmann: Comparing the Expressivity and Usability of Hybrid Systems’ Modeling Languages, Master Thesis, RWTH Aachen University, 2018 (supervisor: Stefan Schupp, Theory of Hybrid Systems research group)
  • Frank Emrich: Modular Static Analysis of LLVM Programs by Symbolic Execution, Master Thesis, RWTH Aachen University, 2018 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Timo Bergerbusch: Geometric Non-Termination Arguments for Integer Programs, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Philipp Görick: Matrix Properties in Type Systems of Component and Connector Based Languages, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Evgeny Kusmenko, Lehrstuhl Informatik 3)
  • Sven Titz: Extension of a Static Value Range Analysis for Matlab/Simulink Models by Block Abstractions, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Norman Hansen, Lehrstuhl Informatik 11)
  • Fabian Kahlert: Extension of the C&C View Language and its Verification for Embedded Systems, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Michael von Wenckstern, Lehrstuhl Informatik 3)
  • Marc Wiartalla: Compositional Modelling and Verification of Distributed Systems with Special Composition Operators, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Deni Raco, Lehrstuhl Informatik 3)
  • Dennis Slotboom: Ein Verifikationsframework for Zeitsensitive Verteilte Systeme, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Deni Raco, Lehrstuhl Informatik 3)
  • Jens Bürger: Modular Hierarchical Modeling and Verification of Systems with General Composition Operators, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Deni Raco, Lehrstuhl Informatik 3)
  • Fabian Grewing geb. Heimbürger: Symbolic Distributed Execution of MPI Programs, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Oscar Dustmann, Lehrstuhl Informatik 4)
  • Marko van Treeck: Symbolic Execution of Concurrent Industrial Applications, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Oscar Dustmann, Rene Glebke, Lehrstuhl Informatik 4)
  • Sven Deserno: Probabilistic Model Checking for Markov Chain Families, Master Thesis, RWTH Aachen University, 2017 (supervisor: Sebastian Junges, Lehrstuhl Informatik 2)
  • Ferdinand Mehlan: Verification of Non-Functional Properties on Component and Connector Models, RWTH Aachen University, 2017 (supervisor: M. von Wenckstern, Lehrstuhl Informatik 3)
  • Oliver Hildebrandt: Extending Component-and-Connector-Views with Component Types Syntactically and Semantically, RWTH Aachen University, 2017 (supervisor: M. von Wenckstern, Lehrstuhl Informatik 3)
  • Maximilian Sistemich: Symbolic Execution of BPF Bytecode in the Realm of Network Function Virtualization, Bachelor Thesis, RWTH Aachen University, 2017 (supervisors: Oscar Dustamann, Daniel Schemmel, Lehrstuhl Informatik 4)
  • Kevin Batz: Proof Rules for Expected Runtimes of Probabilistic Programs, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • David Kräutmann: Refining Heap-Shape Information for Java Programs using Reachable Types, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Florian Frohn, LuFG Informatik 2)
  • Dustin Jungen: Repairs in Dynamic Fault Trees, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Sebastian Junges, Lehrstuhl Informatik 2)
  • Marc Summen: Sprachinklusion von Produkten zeitbehafteter Automaten, Bachelor Thesis, RWTH Aachen University, 2017 (supervisor: Marc Förster, Lehrstuhl Informatik 11)
  • Mohamed Shaaban: Iterative Static Analysis for PLC Code During Development, Master Thesis, RWTH Aachen University, 2017 (supervisor: Mathias Obster, Hendrik Simon, Lehrstuhl Informatik 11)
  • Oliver Westphal: Approximative Transformation of Java Programs for Automated Termination Analysis, Master Thesis, RWTH Aachen University, 2017 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Michael Deutschen: Petri Net Semantics for Dynamic Fault Trees, Master Thesis, RWTH Aachen University, 2016 (supervisors: Sebastian Junges, Matthias Volk, Lehrstuhl Informatik 2)
  • Ronja Nocon: Pattern-Based Analysis of Monotonicity on Dynamic Fault Trees, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Sebastian Junges, Lehrstuhl Informatik 2)
  • Philipp Berger: Game-Based Abstraction of Parametric Markov Models, Master Thesis, RWTH Aachen University, 2016 (supervisor: Christian Dehnert, Lehrstuhl Informatik 2)
  • Robert Funk: Policy Iteration for Static Analysis of PLC Programs, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Marcus Völker, Lehrstuhl Informatik 11)
  • Vincent Drury: Complex Event Processing over Event Streams in Learning Games, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Prof. Schroeder, LuFG Informatik 9)
  • Tim Quatmann: Multi-Objective Model Checking of Markov Automata, Master Thesis, RWTH Aachen University, 2016 (supervisor: Matthias Volk, Lehrstuhl Informatik 2)
  • Julian Büning: Incorporating Liveness Violation Testing into Symbolic Execution, Bachelor Thesis, RWTH Aachen University, 2016 (supervisors: Oscar Dustmann, Daniel Schemmel, Lehrstuhl Informatik 4)
  • Alexander Hoppen: Proving Non-Termination of LLVM Programs using Integer Transition Systems, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Jera Hensel, LuFG Informatik 2)
  • Ralf Bettermann: Identifying Suitable Computations for Fully Automatic Memoization of Simulation Parameter Studies, Master Thesis, RWTH Aachen University, 2016 (supervisor: Mirko Stoffers, Lehrstuhl Informatik 4)
  • Nico Koprowski: Automatic Testing for Atomicity Violation in Parallelized Code Regions, Master Thesis, RWTH Aachen University, 2016 (supervisor: Prof. Wolf, TU Darmstadt)
  • Felix Frei: Acyclicity Analysis for Java, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Felix Rath: Abstract Memory Layout for Symbolic Execution, Master Thesis, RWTH Aachen University, 2016 (supervisor: Prof. Wehrle, Lehrstuhl Informatik 4)
  • Simon Feiden: Extending Probability Generating Function Semantics to Negative Variable Valuations, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Benjamin Kaminski, Lehrstuhl Informatik 2)
  • David Korzeniewski: McMillan Prefixes for Stochastic Petri Nets, Master Thesis, RWTH Aachen University, 2016 (supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • Thies Strothmann: Termination Analysis for Concurrent Java Programs, Bachelor Thesis, RWTH Aachen University, 2016 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Felix Bier: Automatic Time Complexity Analysis of Java Programs, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Manuel Weiand: Checking Reachability Properties in Parametric MDPSs, Master Thesis, RWTH Aachen University, 2015 (supervisor: Christian Dehnert, Lehrstuhl Informatik 2)
  • Lukas Armborst: Generating Simulink Models from AADL System Descriptions, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Harold Bruintjes, Lehrstuhl Informatik 2)
  • Christof Mroz: Static Analysis of PLC Programs using Relational Domains, Master Thesis, RWTH Aachen University, 2015 (supervisor: Hendrik Simon, Lehrstuhl Informatik 11)
  • Marco Grochowski: Efficient Encoding of PLC Programs for NuXMV, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Dimitri Bohlender, Lehrstuhl Informatik 11)
  • Christopher Czyba: Static Analysis of Sequential Function Charts, Master Thesis, RWTH Aachen University, 2015 (supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Clara Scherbaum: Probability Generating Function Semantics for Probabilistic Programs, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Benjamin Kaminski, Lehrstuhl Informatik 2)
  • Lukas Westhofen: On-the-fly Model Checking of Probabilistic Programs, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Dr. Nils Jansen, Lehrstuhl Informatik 2)
  • Hermann Walth: LLVM Nontermination Analysis, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Justin Winkens: Loop Invariants in Probabilistic Programs, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Friedrich Gretz, Lehrstuhl Informatik 2)
  • Manuela Dalibor: Hierarchische Specifikations-Automaten, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Hendrik Simon, Lehrstuhl Informatik 11)
  • Sascha Kurowski: Qualitative Model Checking of Markov Decision Processes on GPUs, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Christian Dehnert, Lehrstuhl Informatik 2)
  • Thomas Henn: Detecting Irrelevant Code in Java Bytecode Programs Automatically, Bachelor Thesis, RWTH Aachen University, 2015 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Tuan Nguyen: Parallelization and Optimization of a Data Dependence Profiler, Master Thesis, RWTH Aachen University, 2014 (supervisor: Dr. Jannesari, German Research School for Simulation Sciences)
  • Lisa von Büttner: Probabilistic Backward Simulation on Interactive Markov Chains, Master Thesis, RWTH Aachen University, 2014 (supervisor: Christian Dehnert, Lehrstuhl Informatik 2)
  • Kai Driessen: Modular Verification for PLC-Controlled Hybrid Systems, Master Thesis, RWTH Aachen University, 2014 (supervisor: Johanna Nellen, Theory of Hybrid Systems research group)
  • Nico Friedrich: Precise Counterexample Generation for Programmable Logic Controllers, Bachelor Thesis, RWTH Aachen University, 2014 (supervisor: Sebastian Biallas, Lehrstuhl Informatik 11)
  • Jera Hensel: Analyzing Alignment and Modulo Calculation in LLVM Programs, Master Thesis, RWTH Aachen University, 2014 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Daniel Schemmel: Automated Memoization for Complex Impure Languages using the Example of C++, Master Thesis, RWTH Aachen University, 2014 (supervisors: Mirko Stoffers, Oscar Dustmann, Lehrstuhl Informatik 4)
  • Dimitri Bohlender: Accelerating Predicate Abstractions for Probabilistic Automata, Master Thesis, RWTH Aachen University, 2014 (supervisor: Christian Dehnert, Lehrstuhl Informatik 2)
  • Cornelius Aschermann: Heap Invariants in Termination Graphs for LLVM, Master Thesis, RWTH Aachen University, 2014 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Sergey Sazonov: Property Preservation under Bisimulation on Markov Automata, Master Thesis, RWTH Aachen University, 2014 (supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • Ernst Wrtal: SCPC Secure Crypto-Protocol System: Der Compiler, Diplomarbeit, RWTH Aachen University, 2013 (co-supervisor: Dr. Unger, Lehrstuhl Informatik 1)
  • Julian Becker: Überwachung von Datenzugriffen in C-Programmen während des Assembly-Model-Checkings, RWTH Aachen University, 2013 (supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Stefan Gottschalk: Modellbasiertes Testen von AADL-Modellen mit Echtzeit, Diplomarbeit, RWTH Aachen University, 2013 (supervisor: S. von Styp, Lehrstuhl Informatik 2)
  • Mathias Obster: Ausführung und Simulation von SPS-Programmen auf RTAndroid, Master Thesis, RWTH Aachen University, 2013 (supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Alexander Braining: Model-Checking von Automaten-basierter Spezifikationen für eingebettete Systeme, Masterarbeit, RWTH Aachen University, 2013 (supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Felix Weßendorf: SCPS Secure Crypto-Protocol System: Die Laufzeitumgebung, Diplomarbeit, RWTH Aachen University, 2013 (supervisor: Dr. Unger, Lehrstuhl Informatik 1)
  • Oscar Dustmann: Symbolic Execution of Discrete-Event Systems with Uncertain Time, Master Thesis, RWTH Aachen University, 2012 (supervisor: R. Sasnauskas, Lehrstuhl Informatik 4)
  • Marcus Völker: Control Flow and Value Set Analysis using SMT Solving, Bachelor Thesis, RWTH Aachen University, 2012 (supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Alexander Weinert: Inferring Heap Abstraction Grammars, Bachelorarbeit, RWTH Aachen University, 2012 (supervisor: J. Heinen, Lehrstuhl Informatik 2)
  • Hussein Hamid Baagil: Quantitative Message Sequence Charts, Diplomarbeit, RWTH Aachen University, 2012 (supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • Nguyen Ngo Bao-Loc: Context-Sensitive Autocompletion in the UML/P, Bachelorarbeit, RWTH Aachen University, 2012 (supervisor: Prof. Rumpe, Lehrstuhl Informatik 3)
  • Dimitri Bohlender: Modulare und Boolesche Abstraktion von SPS-Programmen, Bachelorarbeit, RWTH Aachen University, 2012 (supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Christoph Worreschk: Weighted Lumpability on Markov Chains, Bachelorarbeit, RWTH Aachen University, 2012 (supervisor: Arpit Sharma, Lehrstuhl Informatik 2)
  • Mircea Gherzan: Optimizations for Packet Filters, Masterarbeit, RWTH Aachen University, 2012 (supervisor: Prof. Wehrle, Lehrstuhl  Informatik 4)
  • Jonas Dederichs: Visualization of Abstracted States of the Java Virtual Machine, Bachelorarbeit, RWTH Aachen University (ongoing; supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • Michael Lambertz: Development of Data Abstractions by Combining Bit and Interval Domains in Explicit Model Checking of Embedded Systems, Diplomarbeit, RWTH Aachen University (ongoing; supervisor: J. Brauer, Lehrstuhl Informatik 11)
  • Sebastian Schmitz: Optimierung einer oktagonbasierten Wertebereichsanalyse durch Lokalisierung abstrakter Speicherstellen, RWTH Aachen University, 2012 (supervisor: E. Beckschulze, Lehrstuhl Informatik 11)
  • Birgit Tamkus: CTL Model Checking of Abstract State Spaces Using Three-Valued Atomic Propositions, Diplomarbeit, RWTH Aachen University, 2012 (supervisor: J. Brauer, Lehrstuhl Informatik 11)
  • Cornelius Aschermann: Ein Codeanalysetool für Ruby-Sicherheitsaudits, Bachelorarbeit, RWTH Aachen University, 2011 (supervisor: Prof. Meyer, UMIC Research Centre)
  • Silvio De Carolis: Zuverlässigkeitsanalyse dynamischer Fehlerbäume, Masterarbeit, RWTH Aachen University, 2011 (supervisor: Prof. Katoen, Lehrstuhl Informatik 2)
  • Henrik Barthels: Automata-Based Detection of Hypergraph Embeddings, Bachelorarbeit in Elektrotechnik und Informationstechnik, RWTH Aachen University, 2011 (first reviewer: Prof. Mathar, Lehrstuhl Theoretische Informationstechnik; supervisor: J. Heinen, Lehrstuhl Informatik 2)
  • Na Bai: Datenflussanalysen für speicherprogrammierbare Steuerungen, Diplomarbeit, RWTH Aachen University, 2011 (supervisor: J. Brauer, Lehrstuhl Informatik 11)
  • Mustafa Karafil: Analyse von indirektem Kontrollfluss in Microcontroller-Software, Diplomarbeit, RWTH Aachen University, 2011 (supervisor: J. Brauer, Lehrstuhl Informatik 11)
  • Frank Birbacher: Relationale statische Analyse von AWL-Programmen mittels Kongruenzen, Diplomarbeit, RWTH Aachen University, 2011 (supervisor: J. Brauer, Lehrstuhl Informatik 11)
  • Tim Enger: Nicht-Terminierung schleifenfreier Termersetzungssysteme, Bachelorarbeit, RWTH Aachen University, 2010 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Sebastian Weise: Outermost-Terminierung von Termersetzungssystemen, Diplomarbeit, RWTH Aachen University, 2010 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Sebastian Biallas: Counterexample-Guided Abstraction Refinement for Programmable Logic Controllers, Diplomarbeit, RWTH Aachen University, 2010 (supervisor: Dr. Schlich, Lehrstuhl Informatik 11)
  • Tobias Vaegs: Design and Implementation of a Statistical Vector-based Routing Protocol, Diplomarbeit, RWTH Aachen University, 2010 (supervisor: Prof. Wehrle, LuFG Informatik 4)
  • Jörg Toborg: Static Analysis of Assembly Code for the Renesas R8C/23 Microcontroller, Diplomarbeit, RWTH Aachen University, 2010 (supervisor: J. Brauer, Lehrstuhl Informatik 11)
  • Lucas Brutschy: Static Analysis of Microcontroller Programs by SAT and Constraint Solving, Bachelor Thesis, RWTH Aachen University, 2009 (supervisor: J. Brauer, Lehrstuhl Informatik 11)
  • Mudassir Rasool: Model Checking Programs for the Renesas R8C/23 Microcontroller using mc[square], Master Thesis, RWTH Aachen University, 2009 (supervisor: Dr. Schlich, Lehrstuhl Informatik 11)
  • Jiemin Zhang: Analyse und Visualisierung von flex und bison Automaten, Diplomarbeit, RWTH Aachen University, 2008 (supervisor: Prof. Naumann, LuFG Informatik 12)
  • Stefan Mau: Paralleler und verteilter Aufbau des Zustandsraums im Model Checker [mc]square, Diplomarbeit, RWTH Aachen University, 2008 (supervisor: Dr. Schlich, Lehrstuhl Informatik 11)
  • Volker Kamin: Erweiterung der symbolischen Zustandsdarstellung in [mc]square, Diplomarbeit, RWTH Aachen University, 2008 (supervisor: Dr. Schlich, Lehrstuhl Informatik 11)
  • Patrick Wiehe: Automated Termination Analysis by Semantic Labelling on Infinite Domains, Diplomarbeit, RWTH Aachen University, 2008 (supervisor: Prof. Giesl, LuFG Informatik 2)
  • Wei Zhong: Abhängigkeitsanalyse in parallelisierenden Compilern, Diplomarbeit, RWTH Aachen University, 2008 (supervisor: Prof. Naumann, LuFG Informatik 12)
  • Anupam Kaul: On-Line Matching of Semantic Web Services in Ambient Intelligence Environments, Master Thesis, RWTH Aachen University, 2006 (first reviewer: Prof. Spaniol, Lehrstuhl Informatik 4)
  • Gustavo Arturo Quiros Araya: Static Byte-Code Analysis for State Space Reduction, Master Thesis, RWTH Aachen University, 2006 (supervisor: Prof. Kowalewski, Lehrstuhl Informatik 11)
  • Clara Benac Earle: Model Checking the Interaction of Erlang Components, PhD Thesis, University of Kent, GB, 2005 (first reviewer: Prof. Bowman, University of Kent)
  • Stefan Schürmans: Ein Compiler und eine Virtuelle Maschine zur Zustandsraumgenerierung, Diplomarbeit, RWTH Aachen University, 2005 (supervisor: Prof. Indermark, Lehrstuhl Informatik 2 )
  • Sven Dorf: Transaktionsbasierte Anomalieerkennung für sicherheitsrelevante System- und Anwendungsprozesse, Diplomarbeit, RWTH Aachen University, 2000 (supervisor: R. Büschkes, Lehrstuhl Informatik IV)
  • Mark Borning: Transaktionsbasierte Anomalieerkennung in Kommunikationsnetzen, Diplomarbeit, RWTH Aachen University, 1999 (supervisor: R. Büschkes, Lehrstuhl Informatik IV)