Student Projects
We are constantly offering topics on all levels in our research areas.
Come see us to discuss your individual interests.
Contact: Bernd Finkbeiner
Topic Areas
- Verification
- Temporal Logic
- Program Synthesis
- Runtime Monitoring
- Hyperproperties
- Machine Learning for Formal Methods
- Neuro-symbolic computing
- Formally verified static analyzers and compilers
- Automata and Game Theory
Past Student Projects
- Mohamed Ghanem, NeuRes: A Neural Resolution Prover of Unsatisfiability, Master Thesis, 2024
- Felix Jahn, Counterfactual Causality in Real-Time Systems, Master Thesis, 2023
- Tobias Wagenpfeil, Runtime Verification for Algorithmic Fairness, Bachelor Thesis, 2023
- Peter Gastauer, Structured Program Synthesis from Temporal Stream Logic Specifications, Bachelor Thesis, 2023
- Paul Eichler, RTLola in the Cloud: Reliability for Cloud Applications using Runtime Verification, Bachelor Thesis, 2023
- Katharina Buchthal, RTLola App, Student Project (Hiwi), 2022
- Jonas Linn, Refinement of TSL Specifications for LTL Synthesis, Bachelor Thesis, 2022
- Janine Lohse, Model Checking Temporal Stream Logic and Hyper-Temporal Stream Logic, Bachelor Thesis, 2022
- Sanny Schmitt, An Efficient Automaton Construction for Synthesizing Dominant Strategies, Master Thesis, 2022
- Stefan Oswald, Model-Refinement via Runtime Monitoring, Master Thesis, 2022
- Jessica Schmidt, Runtime Monitoring of Neural Networks for Safe Autonomous Driving, Master Thesis, 2022
- Jan-Robin Aumann, Modularization of code in RTLola, Bachelor Thesis, 2022
- Matthias Cosler, Repairing Circuits with Transformers, Master Thesis, 2022
- Florian Bies, Complete Bounded Model Checking for Hyperproperties, Bachelor Thesis, 2022
- Jonas Birtel, Evaluation of Vulnerabilities of a Lane Keeping Assist System based on Simulations, Bachelor Thesis, 2022
- Jens Kreber, Generating and Solving Temporal Logic Problems with Adversarial Transformers, Master Thesis, 2022
- Ayham Omar, Predicting Timed Traces with Neural Networks, Bachelor Thesis, 2022
- Leonard Niemann, Outlier Prediction in Image Streams, Bachelor Thesis, 2021
- Rafael Dewes, Monitoring HyperMTL, Master Thesis, 2021
- Julia Laichner, Timing is Key – A WCET Analysis of RTLola, Bachelor Thesis, 2021
- Frederik Scheerer, Monitoring Smart Contracts with RTLola, Bachelor Thesis, 2021
- Simon Engel, Bounded Model Checking for PHL, Bachelor Thesis, 2021
- Florian Bies, MCHyper Reimplementation: Conception and Execution, Student Project (Hiwi), 2021
- Lukas Auer, MCHyper Reimplementation: Conception, Student Project (Hiwi), 2021
- Tobias Hans, Algorithms for Deciding HyperCTL*, Master Thesis, 2021
- Jessica Schmidt, Robust Runtime Verification for Medical CPS, Bachelor Thesis, 2021
- Julian Siber, Causal Solving of Reachability Games, Master Thesis, 2021
- Frederik Schmitt, LTL Synthesis from Specification Patterns with Neural Networks, Master Thesis, 2021
- Daniel Schäfer, Synthesizing Epistemic Specifications Using LTL Synthesis, Master Thesis, 2020
- Julia Tillman, Temporal Stream Logic for Hyperproperties, Bachelor Thesis, 2020
- Gideon Geier, Specification Decomposition for Reactive Synthesis, Bachelor Thesis, 2020
- Philippe Heim, Satisfiability of Temporal Stream Logic modulo Theories, Bachelor Thesis, 2020
- Carsten Gerstacker, Trajectory Prediction with RNNs, Master Thesis, 2020
- Stefan Oswald, Verifiable Runtime Monitor Generation for Lola Specifications, Bachelor Thesis, 2020
- Jan Baumeister, Tracing Correctness: A Practical Approach to Traceable Runtime Monitoring, Master Thesis, 2020
- Niklas Metzger, Live Synthesis, Master Thesis, 2019
- Norine Coenen, Verifying Hyperliveness, Master Thesis, 2019
- Noemi Passing, Compositional Synthesis of Dominant Strategies for Distributed Systems, Master Thesis, 2019
- Maximilian Schwenger, Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS, Master Thesis, 2019
- Matthias Cosler, Towards Synthesizing Smart Contracts: Reducing ATL* Synthesis to HyperLTL Synthesis, Bachelor Thesis, 2019
- Paul Bungert, Monitoring Hybrid Automata, Bachelor Thesis, 2019
- Raven Beutner, Translating Asynchronous Games for Distributed Synthesis, Bachelor Thesis, 2019
- Hendrik Leidinger, Learning the Desired Behavior for Causality Analyses, Master Thesis, 2019
- Florian Kohn, A Stream-based Approach to Network Intrusion Detection, Bachelor Thesis, 2019
- Julian Siber, Causality-Based Model Checking for Real-Time Systems, Bachelor Thesis, 2019
- Christoph Rosenhauer, Compiling Lola 2.0 to C, Bachelor Thesis, 2019
- Sanny Schmitt, Generating Concurrency-preserving Petri Games, Bachelor Thesis, 2019
- Benedict Strube, MCHyper Online Interface: Frontend, Student Project (Hiwi), 2018
- Jens Kreber, MCHyper Online Interface: Backend, Student Project (Hiwi), 2018
- Peter Wita, Bounded Synthesis for Past LTL, Master Thesis, 2018
- Lennart Haas, Learning Hyperproperties, Bachelor Thesis, 2018
- Jens Heinen, Model Checking Timed Hyperproperties, Master Thesis, 2018
- Marvin Hofmann, Runtime Verification of Critical Web-based Systems with Lola, Bachelor Thesis, 2018
- Tobias Hans, MGHyper: Checking Satisfiability of HyperLTL formulas beyond the ∃*∀*-Fragment, Bachelor Thesis, 2018
- Maximilian Köhl, From Knowledge- to Belief-Based Programming for Mobile Ad-Hoc Networks, Bachelor Thesis, 2018
- Valentin Seimetz, Learning Automata for LTL, Bachelor Thesis, 2017
- Nathalie Zeller, Comparing Lola 2.0 with Quantitative Regular Expressions, Bachelor Thesis, 2017
- Marcel Maltry, FPGA-based Monitoring for Stream Specification Languages, Master Thesis, 2017
- Carsten Gerstacker, Bounded Synthesis of Reactive Programs, Bachelor Thesis, 2017
- Jan Baumeister, Encodings of Bounded Synthesis of Distributed Systems, Bachelor Thesis, 2017
- Jannic Warken, Synthesis and Analysis of Strategies for Automatic Parking Garages, Bachelor Thesis, 2017
- Maximilian Köhl, From Knowledge- to Belief-Based Programming for Mobile Ad-Hoc Networks, Bachelor Thesis, 2017
- Niklas Metzger, Bounded Synthesis of Petri Games with True Concurrency Semantics, Bachelor Thesis, 2017
- Paul Gölz, Synthesis for Petri Games with One System Player, Bachelor Thesis, 2017
- Peter Wita, Provable State-Space Minimization of Büchi Automata arising from LTL Specifications, Bachelor Thesis, 2016
- Sebastian Schirmer, Runtime Verification with LOLA, Master Thesis, 2016
- Norine Coenen, A Proof System for HyperLTL, Bachelor Thesis, 2016
- Christopher Hahn, Bounded Synthesis for HyperLTL, Bachelor Thesis, 2016
- Jesko Hecking-Harbusch, Equivalence of Petri Games, Master Thesis, 2016
- Mark Timon Hüneberg, Optimizing LOLA Specifications, Bachelor Thesis, 2015
- Carolyn Guthoff, Bounded Synthesis for Distributed Architectures, Bachelor Thesis, 2015
- Jennifer Niederländer, Approximate LTL Model Counting, Bachelor Thesis, 2015
- Tobias Salzmann, Strategies in Regular Delay Games, Master Thesis, 2015
- Marcel Maltry, Heuristic Algorithms for the Synthesis of AIGER Circuits, Bachelor Thesis, 2015
- Jesko Hecking-Harbusch, A Game-Based Semantis for CSP, Bachelor Thesis, 2015
- Kai Hornung, Monitoring First-order Parametric Temporal Logic, Bachelor Thesis, 2015
- Sebastian Schirmer, A Specification Format for Reactive Synthesis, Bachelor Thesis, 2015
- Felix Klein, Solving Büchi Games, Master Thesis, 2014
- Leander Tentrup, Detecting Unrealizable Specifications of Distributed Systems, Master Thesis, 2013
- Dominik Steiger, Synthesis of Dominant Strategies, Bachelor Thesis, 2013
- Patrick Kelleter, Slicing Abstractions for Modular Programs, Bachelor Thesis, 2013
- Robin Wagner, Slicing Abstractions for Safety Games, Bachelor Thesis, 2013
- Heinrich Ody, Synthesis of Distributed Reactive Programs, Master Thesis, 2013
- Jonas Langhabel, Spin the Records: Synthesizing Electronic Dance Music Using Model Checking Methods, Bachelor Thesis, 2013
- Hazem Torfah, Concept Learning for Reactive Synthesis, Master Thesis, 2013
- Max-Ferdinand Suffel, Acceleration of Timed Automata, Bachelor Thesis, 2012
- Tobias Salzmann, Decidability of Semilinear Petri Games, Bachelor Thesis, 2012
- Leander Tentrup, A compositional proof rule for Extended Coordination Logic, Bachelor Thesis, 2012
- Zhe Fang, Automatische Verifikation von Petri-Netzen mit SLAB, Bachelor Thesis, 2012
- Christian Schömer, Game-based analysis of timed business processes, Bachelor Thesis, 2012
- Daniela Moldovan-Tiglar, Small strategies for safety games, Master Thesis, 2011
- Peter Faymonville, Model Measuring, Master Thesis, 2011
- Michael Gerke, Zone State Diagrams – Model Checking Data-Intensive Real-Time Systems, Master Thesis, 2010
- Daniel Fass, Fully Symbolic Model Checking using Constraint Matrix Diagrams, Master Thesis, 2010
- Markus N. Rabe, Optimal Schedulers for Time-Bounded Reachability in CTMDPs, Master Thesis, 2009
- Daniel Fass, Clock Matrix Diagrams, Bachelor Thesis, 2009
- Daniel Dahrendorf, Symbolic Encodings of Timed Games with Incomplete Information, Master Thesis, 2009
- Andreas Abel, From Uppaal to Slab, Bachelor Thesis, 2009
- Walid Haddad, Verifying Networks of Phase Event Automata, Master Thesis, 2009
- Thomas von Bomhard, Minimization of Tree Automata, Bachelor Thesis, 2008
- Franziska Ebert, Translation Validation for Optimizing Compilers, Master Thesis, 2007
- Martin Bauer, Symbolic Game Solving with Arithmetic Data Types, Bachelor Thesis, 2007
- Dominik Brill, Deductive Model Checking with Transition Constraint Systems, Diploma Thesis, 2007
- Arnaud Fietzke, Learning Minimal Requirements for Compositional Verification, Bachelor Thesis, 2006
- Sven Bünte, Automatic Abstraction of Synchronization Sequences, Bachelor Thesis, 2006
- Hans-Jörg Peter, Controller Program Synthesis for Industrial Machines, Diploma Thesis, 2005
- Jens Regenberg, Synthesis of Reactive Systems, Diploma Thesis, 2005
- Tobias Maurer, Distributed Games For Reactive Systems, Diploma Thesis, 2005
- Pavel Emeliyanenko, Automatic Verification of Conditions for Absence of Interrupts, Bachelor Thesis, 2005
- Ghulam Mujtaba, Monitoring Execution Traces using Metric Alternating Automata, Master Thesis, 2005