Theses

If you are interested in writing a thesis at our research group, please contact us via email.

If you are interested in hybrid systems verification, SMT solving, or probabilistic systems, please contact .
If you are interested in computational renewable energy, please contact .

In your email, please indicate your interests, preferences and prior knowledge and attach a current transcript of records as well as a short, tabular CV/resume. You should have a strong interest in mathematics and formal methods.

We will reply whether we have a suitable topic available and, if yes, set up a meeting with you to discuss it. If you want to write a thesis with us, the best is to contact us early such that we can look for a suitable topic and plan with our capacities accordingly.

Topic areas

We offer topics in the following areas:

Hybrid systems verification

Reachability analysis for hybrid systems
Modelling and analysis of stochastic hybrid systems

SMT solving

Decision procedures for arithmetic theories (both linear and non-linear)
Heuristics for and adaptions of the cylindrical algebraic decomposition for non-linear arithmetic
Novel methods for linear arithmetic
Incomplete methods for non-linear arithmetic and their combination with complete methods
Implementation in our SMT solver SMT-RAT

Probabilistic systems

Verification of probabilistic hyperproperties

Computational renewable energy

Heuristic layout optimization for solar thermal power plants

In the following lists of running and completed theses you can find exemplary previous topics.

In progress

Max Backhaus, “TBD” (Bachelor thesis, supervision Erika Ábrahám)
Murad Bayramli, “Automatische Generierung von parametrischen Aufgaben für Datenstrukturen und Algorithmen” (Bachelor thesis, supervision Erika Ábrahám)
Kim Bohn, “Approximative quantifier elimination for linear real algebraic constraint sets” (Master thesis, supervision Erika Ábrahám)
Arda Celik, “Optimization-based wind farm planning: Abstraction and efficiency of layout algorithms” (Bachelor thesis, supervision Erika Ábrahám)
Carsten Perkampus, “Formalizing a proof system for single cell construction in lean” (Master thesis, supervision Erika Ábrahám, Jasper Nalbach, Valentin Promies)
Erdzan Rastoder, “Optimizing solar panel installation and assessing rooftop solar energy potential” (Master thesis, supervision Erika Ábrahám, Pascal Richter)
Gino Urban, “Development of a techno-economic optimization model for utility-scale photovoltaic systems” (Master thesis, supervision Erika Ábrahám, Pascal Richter)

Completed

2026

Dilara Arslan, “Extending the RealySt tool to support linear hybrid automata” (Bachelor thesis 2026, supervision Erika Ábrahám, József Kovács) [slides]
Daniel Braun, “Analysis and verification of the Frandsen turbulence model for wind turbine site suitability assessment” (Bachelor thesis 2026, supervision Erika Ábrahám, Pascal Richter) [slides]
Yvonne Heimowski, “Solving initial-state non-determinism in stochastic linear hybrid automata with under-approximative backwards refinement” (Master thesis 2026, supervision Erika Ábrahám, József Kovács) [slides]
Andre Hofer, “Real-time scan-to-BIM on edge devices: Extending RoomPlan for radiator detection and reconstruction” (Master thesis 2026, supervision Erika Ábrahám)
Florian Corvin Hoffmann, “Determination of potential areas for wind power considering shadow flicker and sound propagation” (Bachelor thesis 2026, supervision Erika Ábrahám, Pascal Richter)
Matteo Ludwig, “Automatic dimensioning and efficiency optimization of heating systems” (Master thesis 03/2026, supervision Erika Ábrahám, Pascal Richter) [slides]
Dennis Winter, “Fast heliostat field evaluation and pattern shaping for central receiver systems” (Master thesis 2026, supervision Erika Ábrahám, Pascal Richter)

2021

Lukas Aldenhoff, “Raytracer for central receiver systems using GPU” (Master thesis 06/2021, supervision Pascal Richter, Erika Ábrahám)
Kim Amfaldern, “Computing set difference for the reachability analysis of hybrid systems” (Bachelor thesis 11/2021, supervision Erika Ábrahám)
Matthias Appenzeller, “Comparing two modeling formalisms for stochastic hybrid systems” (Bachelor thesis 05/2021, supervision Erika Ábrahám)
Marian Assenmacher, “Parallelization of a probabilistic railway timetable simulation” (Master thesis 05/2021, supervision Erika Ábrahám, Rebecca Haehn)
Thomas Bauer, “Quantifier elimination for real-arithmetic problems with Boolean structure using the Fourier-Motzkin method” (Bachelor thesis 2021, supervision Erika Ábrahám, Jasper Nalbach)
László Dirks, “A CEGAR approach for efficient planning” (Bachelor thesis 09/2021, supervision Erika Ábrahám, Francesco Leofante)
Tristan Ebert, “CEGAR approach for handling urgency in hybrid systems” (Master thesis 11/2021, supervision Erika Ábrahám)
Mostafa Elgayar, “Interactive visualization of shadow cast for wind farms” (Bachelor thesis 09/2021, supervision Pascal Richter, Erika Ábrahám)
Antoniu-Paul Filip, “Automated exercise generation for satisfiability modulo real algebra” (Bachelor thesis 10/2021, supervision Erika Ábrahám)
Lars Fischer, “Multi-step layout optimization of heliostat fields in central receiver systems” (Bachelor thesis 02/2021, supervision Pascal Richter, Erika Ábrahám)
Menghze Hua, “Approximate model checking for probabilistic rectangular automata with continuous-time probability distributions on jumps” (Master thesis 05/2021, supervision Erika Ábrahám, Stefan Schupp)
Laura-Sophie Kirchner, “Automation and investigation of multi output machine learning control in buildings” (Master thesis 09/2021, supervision Ahmed Abida, Erika Ábrahám)
Paul Kobialka, “Connecting simplex and Fourier-Motzkin into a novel quantifier elimination method for linear real algebra” (Master thesis 07/2021, supervision Erika Ábrahám, Jasper Nalbach)
Niklas Kotowski, “Accelerating symbolic simulation to analyze the effect of delays in train timetables” (Master thesis 09/2021, supervision Erika Ábrahám, Rebecca Haehn)
Stefan Leachu, “Optimal building control using system linearization based on a generalized physics model” (Master thesis 03/2021, supervision Erika Ábrahám, Ahmed Abida)
Dana Lenz, “Flexible encoding of scheduling problems using satisfiability modulo theories” (Bachelor thesis 2021, supervision Erika Ábrahám)
Wei Lu, “Visualizing stochastic delay information for railway timetables” (Master thesis 07/2021, supervision Erika Ábrahám)
Christoph von Oy, “Optimal design and scheduling of a smart city under uncertain renewable energy generation” (Master thesis 07/2021, supervision Pascal Richter, Erika Ábrahám)
Viktor Panichkin, “Auralization and visualization of wind farms using augmented reality” (Master thesis 07/2021, supervision Pascal Richter, Erika Ábrahám)
André Poncelet, “Conflict generalization for quadratic real-arithmetic constraints in SMT-RAT” (Bachelor thesis 12/2021, supervision Erika Ábrahám, Jasper Nalbach)
Boris Schüpp, “Quantifier elimination using the virtual substitution” (Bachelor thesis 09/2021, supervision Erika Ábrahám, Jasper Nalbach)
Dogu Tamgac, “Star set representations in the reachability analysis of hybrid systems” (Bachelor thesis 11/2021, supervision Erika Ábrahám, Stefan Schupp)
Marvin Thelen, “Quantification of uncertainties and determination of sensitivities for biogeochemical ocean simulations” (Master thesis 04/2021, supervision Pascal Richter, Erika Ábrahám)
Marvin Vogt, “Analysis of probabilistic hybrid automata in HyPro” (Bachelor thesis 03/2021, supervision Erika Ábrahám, Stefan Schupp)
Alexander Wiegel, “A python-based tool using parameter synthesis to find safe and unsafe regions of the parameter space” (Bachelor thesis 09/2021, supervision Erika Ábrahám)
Lukas Wilke, “Probabilistic hyperproperties with rewards” (Bachelor thesis 08/2021, supervision Erika Ábrahám)

2020

Fabian Alieff, “Simplex heuristics in SMT solving” (Bachelor thesis 11/2020, supervision Erika Ábrahám, Jasper Nalbach)
Leander Behr, “Extending flowpipe construction for compositional hybrid automata” (Bachelor thesis 10/2020, supervision Erika Ábrahám, Stefan Schupp)
Serjoscha Bender, “Resource optimized scheduling of scientific solutions on CPU and GPU computing platforms” (Master thesis 12/2020, supervision Pascal Richter, Erika Ábrahám)
Daniel Cloerkes, “Reachability analysis of compositional hybrid systems” (Master thesis 01/2020, supervision Erika Ábrahám, Stefan Schupp)
Hanna Franzen, “Conflict driven cylindrical algebraic coverings for nonlinear arithmetic in SMT solving” (Master thesis 02/2020, supervision Erika Ábrahám, Gereon Kremer)
Jesse Germann, “Optimal climate control in buildings using linear programming” (Bachelor thesis 12/2020, supervision Pascal Richter, Erika Ábrahám)
Zeheng Gong, “Optimal control of volume flow in parabolic trough solar thermal power plants” (Bachelor thesis 12/2020, supervision Pascal Richter, Erika Ábrahám)
Daniel Heinen, “Purging spurious samples in the cylindrical algebraic decomposition” (Bachelor thesis 11/2020, supervision Erika Ábrahám, Jasper Nalbach)
Hang Khuat, “Efficient implementation of HyperPCTL model checking” (Master thesis 07/2020, supervision Erika Ábrahám)
Christian Kiricenko, “Improving the usability and visualization for hybrid systems safety analysis” (Bachelor thesis 03/2020, supervision Erika Ábrahám, Stefan Schupp)
Simon Klemp, “Classification and prediction of thermodynamic value ranges based on geometrical building data” (Bachelor thesis 12/2020, supervision Ahmed Abida, Erika Ábrahám)
Philip Kroll, “Efficient data structures for cylindrical algebraic coverings” (Bachelor thesis 10/2020, supervision Erika Ábrahám, Jasper Nalbach)
Yin-yin Lo, “Multi-step layout optimiation of wind turbines in offshore wind farms” (Bachelor thesis 09/2020, supervision Pascal Richter, Erika Ábrahám)
Frederick Lockemann, “Optimal control strategy for a virtual renewable power plant” (Bachelor thesis 12/2020, supervision Pascal Richter, Erika Ábrahám)
Jasper Nalbach, “A novel adaption of the simplex algorithm for linear real arithmetic” (Master thesis 03/2020, supervision Erika Ábrahám, Gereon Kremer)
Sergej Neuberger, “Safety verification and parameter synthesis for non-linear hybrid systems using Flow*” (Bachelor thesis 03/2020, supervision Erika Ábrahám, Stefan Schupp)
Philippe Specht, “A level-wise variant of single cell construction in cylindrical algebraic decomposition” (Bachelor thesis 09/2020, supervision Erika Ábrahám, Jasper Nalbach)
Nils Speetzen, “Heuristic aiming strategy for solar tower power plants” (Bachelor thesis 08/2020, supervision Pascal Richter, Erika Ábrahám)
Niels von Stein, “Nowcasting of cloud shadows using neural networks” (Master thesis 03/2020, supervision Pascal Richter, Erika Ábrahám)
Phillip Tse, “Template polyhedra in hybrid systems reachability analysis” (Master thesis 04/2020, supervision Erika Ábrahám, Stefan Schupp)
Laurids Vollmann, “Evolutionary optimization of wind farm and heliostat layout” (Master thesis 06/2020, supervision Pascal Richter, Erika Ábrahám)
Hans Vrapi, “Freight train scheduling in bidirectional railway systems” (Bachelor thesis 09/2020, supervision Erika Ábrahám, Rebecca Haehn)

2019

Stella Coumbassa, “Optimal storage strategy for hybrid concentrated solar power – photovoltaic plants” (Master thesis 07/2019, supervision Pascal Richter, Erika Ábrahám)
Julian Düstersiek, “Probabilistic optimization of offshore wind farms” (Bachelor thesis 03/2019, supervision Pascal Richter, Erika Ábrahám)
Marta Grobelna, “Integration of hybrid systems verification methods in Matlab” (Master thesis 09/2019, supervision Erika Ábrahám, Stefan Schupp)
Florian Hövelmann, “Advanced raytracer for solar tower power plants” (Bachelor thesis 10/2019, supervision Pascal Richter, Erika Ábrahám)
Niklas Kotowski, “Application of formal methods in autonomous vehicle control” (Bachelor thesis 07/2019, supervision Erika Ábrahám, Stefan Schupp)
Denis Kuksaus, “SMT-basierte Lösung reell-algebraischer Probleme mittels Linearisierung” (Bachelor thesis 09/2019, supervision Erika Ábrahám, Gereon Kremer)
Marwa Maghnie, “Simulation and optimization of offshore wind farms” (Master thesis 02/2019, supervision Pascal Richter, Erika Ábrahám)
Leon Rabanus, “Probabilistic modeling of robot fleets in production logistics scenarios” (Bachelor thesis 01/2019, supervision Erika Ábrahám, Francesco Leofante)
Kristina Yaneva, “Optimal climate control in buildings using artificial intelligence” (Bachelor thesis 09/2019, supervision Pascal Richter, Erika Ábrahám)
Süleyman Yetim, “Ermittlung von k-kürzesten Wegen im Schienenverkehr zwischen Aachen und Köln” (Bachelor thesis 01/2019, supervision Erika Ábrahám, Rebecca Haehn)
Aklima Zaman, “Incremental linearization for SAT modulo real arithmetic solving” (Master thesis 04/2019, supervision Erika Ábrahám, Gereon Kremer)
Karim Josef Abou Zeid, “Letterplace Gröbner bases, their implementation and applications” (Bachelor thesis 03/2019, supervision Erika Ábrahám, Viktor Levandovskyy)

2018

Lorena Calvo Bartolomé, “Using Fourier-Motzkin variable elimination for MCSAT explanations in SMT-RAT” (Bachelor thesis 09/2018, supervision Erika Ábrahám, Gereon Kremer)
Igor Bongartz, “Explaining unsolvable planning tasks with unsatisfiable cores” (Master thesis 12/2018, supervision Erika Ábrahám, Francesco Leofante)
Linus Franke, “Modelling and optimization of large scale solar tower power plants” (Master thesis 12/2018, supervision Pascal Richter, Erika Ábrahám)
Rebecca Haehn, “Using equational constraints in an incremental CAD projection” (Master thesis 03/2018, supervision Erika Ábrahám, Gereon Kremer)
Jan Hafer, “Using eigenvalue decomposition in hybrid systems reachability analysis” (Bachelor thesis 01/2018, supervision Erika Ábrahám, Stefan Schupp)
Sabrina Kielmann, “Comparing the expressivity and usabiliy of hybrid systems’ modeling languages” (Master thesis 03/2018, supervision Erika Ábrahám, Stefan Schupp)
Christopher Lösbrock, “Implementing an incremental solver for difference logic” (Bachelor thesis 08/2018, supervision Erika Ábrahám, Gereon Kremer, Matthias Volk)
Henri Lotze, “Automated optimization in production planning” (Master thesis 09/2018, supervision Erika Ábrahám, Gereon Kremer)
Tom Neuhäuser, “Quantifier elimination by cylindrical algebraic decomposition” (Bachelor thesis 09/2018, supervision Erika Ábrahám, Gereon Kremer)
Malte Neuß, “Using single CAD cells as explanations in MCSAT-style SMT solving” (Master thesis 09/2018, supervision Gereon Kremer)
Ömer Sali, “Linearization techniques for nonlinear arithmetic problems in SMT” (Master thesis 08/2018, supervision Erika Ábrahám, Gereon Kremer)
Lyudmila Vatskicheva, “Using simulation for counterexample validation in hybrid systems reachability analysis” (Bachelor thesis 03/2018, supervision Erika Ábrahám, Stefan Schupp)
Georg Wicke, “Optimization of aiming strategies for heliostats in solar-thermal power plants” (Bachelor thesis 01/2018, supervision Erika Ábrahám, Pascal Richter)
Justin Winkens, “Context-dependent reachability analysis for hybrid automata” (Master thesis 08/2018, supervision Erika Ábrahám, Stefan Schupp)

2017

Roni Cakar, “Uncertainty quantification of wind farm models” (Bachelor thesis 09/2017, supervision Erika Ábrahám, Pascal Richter)
Marta Grobelna, “Solving pseudo-Boolean constraints” (Bachelor thesis 07/2017, supervision Erika Ábrahám, Gereon Kremer)
Wanja Hentze, “Computing minimal infeasible subsets for the cylindrical algebraic decomposition” (Bachelor thesis 03/2017, supervision Erika Ábrahám, Gereon Kremer)
Leonard Korp, “SMT-based planning for autonomous robot fleets” (Bachelor thesis 08/2017, supervision Erika Ábrahám, Francesco Leofante, Gereon Kremer)
Jasper Nalbach, “Embedding the virtual substitution in the MCSAT framework” (Bachelor thesis 08/2017, supervision Erika Ábrahám)
Lukas Netz, “Analysis on discretization of gene parameters in evolutionary algorithms” (Master thesis 12/2017, supervision Erika Ábrahám, Pascal Richter)

2016

Igor Nicolai Bongartz, “Over-approximative reduction of polytopes in the context of hybrid systems reachability analysis” (Bachelor thesis 02/2016, supervision Erika Ábrahám, Stefan Schupp)
Phillip Florian, “Optimizing reachabiliy analysis for non-autonomous systems using ellipsoids” (Master thesis 09/2016, supervision Erika Ábrahám, Stefan Schupp)
Simon Froitzheim, “Efficient conversion of geometric state set representations for hybrid systems” (Bachelor thesis 05/2016, supervision Erika Ábrahám, Stefan Schupp)
Levin Gerdes, “Generation of probabilistic models for solar thermal power plants” (Master thesis 03/2016, supervision Erika Ábrahám, Martin Frank)
Rebecca Haehn, “Learning control strategies for hybrid vehicles using neural networks” (Bachelor thesis 09/2016, supervision Erika Ábrahám, Johanna Nellen)
Dustin Hütter, “Adaptive dynamic reachability analysis for linear hybrid automata” (Master thesis 09/2016, supervision Erika Ábrahám, Stefan Schupp)
Johannes Neuhaus, “Development of a modular approach for hybrid systems reachability analysis” (Bachelor thesis 09/2016, supervision Erika Ábrahám, Stefan Schupp)
Tarik Viehmann, “Comparing different projection operators in the cylindrical algebraic decomposition for SMT solving” (Bachelor thesis 09/2016, supervision Erika Ábrahám, Gereon Kremer)
Patricia Wessel, “Grid-based control strategy for hybrid vehicles” (Bachelor thesis 09/2016, supervision Erika Ábrahám, Johanna Nellen)
Tobias Winkler, “Using Thom encodings for real algebraic numbers in the cylindrical algebraic decomposition” (Bachelor thesis 09/2016, supervision Erika Ábrahám, Gereon Kremer)

2015

Andreas Krüger, “Bitvectors in SMT-RAT and their application to integer arithmetics” (Master thesis 10/2015, supervision Erika Ábrahám, Gereon Kremer)
Lukas Netz, “Using Horner schemes to improve the efficiency and precision of interval constraint propagation” (Bachelor thesis 09/2015, supervision Florian Corzilius, Stefan Schupp)
Lukas Neuberger, “Generation of infeasible subsets in less-lazy SMT-solving for the theory of uninterpreted functions” (Bachelor thesis 09/2015, supervision Erika Ábrahám, Gereon Kremer)
Matthias Volk, “Using SAT solvers for industrial combinatorial problems” (Master thesis 11/2015, supervision Erika Ábrahám, Florian Corzilius)

2014

Kai Driessen, “Modular verification for PLC controlled hybrid systems” (Master thesis 09/2014, supervision Erika Ábrahám, Johanna Nellen)
Maik Glatki, “A zonotope library for hybrid systems reachability analysis” (Bachelor thesis 01/2014, supervision Erika Ábrahám, Jürgen Giesl)
Dustin Hütter, “SMT solving for linear integer arithmetic” (Bachelor thesis 08/2014, supervision Florian Corzilius, Erika Ábrahám, Jürgen Giesl)
Christopher Kugler, “A polytope library for the reachability analysis of hybrid systems” (Master thesis 09/2014, supervision Stefan Schupp, Erika Ábrahám)

2013

Matthias Ewert, “Modellierung des Radialverdichters eines PKW-Abgasturboladers” (Master thesis 12/2013, supervision Erika Ábrahám, Richard Aymanns, Dominik Lückmann)
Kim Maren Haps, “Datatypes and tools for the analysis of hybrid systems” (Bachelor thesis 06/2013, supervision Johanna Nellen, Erika Ábrahám, Jürgen Giesl)
Georg Jenneßen, “Optimierung eines Heliostatsfeldes unter Einsatz eines genetischen Algorithmus” (Diploma thesis 03/2013, supervision Pascal Richter, Erika Ábrahám, Martin Frank)
Sebastian Junges, “On Gröbner bases in SMT-compliant decision procedures” (Bachelor thesis 02/2013, supervision Erika Ábrahám, Ulrich Loup)
Gereon Kremer, “Isolating real roots using adaptable-precision interval arithmetic” (Master thesis 09/2013, supervision Ulrich Loup, Erika Ábrahám)
Amith Belur Nagabushana, “Minimal critical subsystems for PCTL” (Master thesis 05/2013, supervision Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen)
Henrik Schmitz, “Parallel user-defined strategies for QFNRA” (Diploma thesis 04/2013, supervision Erika Ábrahám, Florian Corzilius)
Stefan Schupp, “Interval constraint propagation in SMT-compliant decision procedures” (Master thesis 03/2013, supervision Erika Ábrahám, Florian Corzilius, Ulrich Loup)
Marian Van de Veire, “Minimal critical subsystems for probabilistic models with nondeterminism” (Diploma thesis 2013, supervision Erika Ábrahám, Nils Jansen, Joost-Pieter Katoen)
Andreas Vorpahl, “Compositional counterexamples for MDPs” (Master thesis 2013, supervision Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen)

2012

Kai Driessen, “Counterexample-guided abstraction refinement for hybrid SFC verification” (Bachelor thesis 09/2012, supervision Erika Ábrahám, Johanna Nellen)
Alin Ionascu, “Modeling and controler synthesis of hybrid propulsion systems using artificial intelligence” (Master thesis 11/2012, supervision Erika Ábrahám, Johanna Nellen, Ulrich Loup)
Canan Kasaci, “Model-based resource monitoring and optimization” (Master thesis 01/2012, supervision Erika Ábrahám, Stefan Kowalewski, ASML)
Thomas Osterland, “Memory- and time-related action qualifiers in HSFCs” (Bachelor thesis 12/2012, supervision Erika Ábrahám, Johanna Nellen)
Joachim Redies, “An extension of the GiNaCRA library for the cylindrical algebraic decomposition” (Bachelor thesis 01/2012, supervision Erika Ábrahám, Ulrich Loup, Peter Rossmanith)
Maik Scheffler, “Hierarchical counterexamples for DTMCs – Case studies” (Diploma thesis 2012, supervision Erika Ábrahám, Nils Jansen)
Dennis Scully, “Preprocessing for solving non-linear real-arithmetic formulas” (Bachelor thesis 09/2012, supervision Erika Ábrahám, Florian Corzilius)
Matthias Volk, “Verification and synthesis for parametric Markov chains” (Bachelor thesis 09/2012, supervision Erika Ábrahám, Nils Jansen, Florian Corzilius)

2010

Florian Corzilius, “Virtual substitution in SMT solving” (Diploma thesis 12/2010, supervision Erika Ábrahám, Ulrich Loup)

2009

Pascal Richter, “Simulation und Auslegungsoptimierung solarthermischer Kraftwerke unter Einsatz evolutionärer Algorithmen und neuronaler Netze” (Diploma thesis 12/2009, supervision Erika Ábrahám, Volker Wittwer)