Theses

Available topics

Below we list some exemplary  topics for theses. Please contact us if you are interested in these or similar topics.

Hybrid systems verification

  • Safety analysis for hybrid systems with random/uncertain components (contact: Erika Abraham)

SMT solving

  • Automated exercise generation for SMT solving (contact: Erika Abraham)
  • Developing, implementing and evaluating different variable ordering heuristics for arithmetic theory decision procedures in SMT solving (contact: Erika Abraham)
  • Using dyadic rationals for the representation of real algebraic numbers (contact: Jasper Nalbach)
  • Approximating cell boundaries in the cylindrical algebraic decomposition (contact: Jasper Nalbach)
  • Generating proofs for real algebra (contact: Jasper Nalbach)
  • Solving uninterpreted functions within the model-constructing satisfiability calculus (contact: Jasper Nalbach)
  • A novel improvement for the virtual substitution decision procedure for linear real arithmetic (contact: Erika Abraham)
  • Synthesizing controllers for robot fleets in production logistics scenarios using SMT solving (contact: Erika Abraham)
  • Extending the SMT-LIB2 benchmark library for non-linear real and integer arithmetic (contact: Erika Abraham)
  • Generating explanations for unsatisfiability in SMT solving (contact: Erika Abraham)
  • The development and implementation of a theory solver module for floating-point arithmetic in the SMT solver library SMT-RAT (contact: Erika Abraham)

Probabilistic systems

  • Why is your train delayed? — Analyzing and visualizing reasons for delay effects in timetables (contact: Rebecca Haehn,  Erika Abraham)

Computational Renewable Energy
Contact: Pascal Richter

  • Augmented reality for the planning of wind farms [PDF]
  • App Development for Children in Primary School [PDF]
  • Optimal Storage Strategy for Central Receiver Systems [PDF]
  • Web application for the simulation of offshore and onshore wind farms [PDF]
  • Dynamic aiming strategy for central receiver systems [PDF]

Smart Building
Contact: Ahmed Abida

  • Smart building – Optimized control for climate in buildings [PDF]

Miscellaneous

In progress

Please ask your supervisor for our checklist with information for thesis students.

  1. Kim Amfaldern, “Computing set difference for the reachability analysis of hybrid systems” (Bachelor thesis, supervision Erika Ábrahám)
  2. Thomas Bauer, “Quantifier elimination for real-arithmetic problems with Boolean structure using the Fourier-Motzkin method” (Bachelor thesis, supervision: Erika Ábrahám, Jasper Nalbach)
  3. László Dirks, “A CEGAR approach for efficient planning” (Bachelor thesis, supervision: Erika Ábrahám, Francesco Leofante)
  4. Tristan Ebert, “CEGAR approach for handling urgency in hybrid systems” (Master thesis, supervision: Erika Ábrahám)
  5. Antoniu-Paul Filip, “Automated exercise generation for satisfiability modulo real algebra” (Bachelor thesis, supervision Erika Ábrahám)
  6. Celina Kalus, “TBA” (Bachelor thesis, supervision Erika Ábrahám)
  7. Niklas Kotowski, “Accelerating symbolic simulation to analyze the effect of delays in train timetables” (Master thesis, supervision: Erika Ábrahám, Rebecca Haehn)
  8. Dana Lenz, “TBA” (Bachelor thesis, supervision Erika Ábrahám)
  9. André Poncelet, “Generating virtual substitution-based coverings within the model-constructing satisfiability calculus” (Bachelor thesis, supervision Erika Ábrahám, Jasper Nalbach)
  10. Nadja Scherer, “TBA” (Bachelor thesis, supervision Erika Ábrahám)
  11. Boris Schüpp, “Quantifier elimination using the virtual substitution” (Bachelor thesis, supervision Erika Ábrahám, Jasper Nalbach)
  12. Svenja Stein, “TBA” (Bachelor thesis, supervision Erika Ábrahám)
  13. Dogu Tamgac, “Star set representations in the reachability analysis of hybrid systems”, (Bachelor thesis, supervision Erika Ábrahám, Stefan Schupp)
  14. Alexander Wiegel, “A python-based tool using parameter synthesis to find safe and unsafe regions of the parameter space” Bachelor thesis, supervision Erika Ábrahám)

Completed

2021

  1. Lukas Aldenhoff, “Raytracer for central receiver systems using GPU” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
  2. Matthias Appenzeller, “Comparing two modeling formalisms for stochastic hybrid systems” (Bachelor thesis, supervision Erika Ábrahám)
  3. Marian Assenmacher, “Parallelization of a probabilistic railway timetable simulation” (Master thesis, supervision: Erika Ábrahám, Rebecca Haehn)
  4. Leander Behr, “Extending flowpipe construction for compositional hybrid automata” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
  5. Mostafa Elgayar, “Interactive visualization of shadow cast for wind farms” (Bachelor thesis, supervision: Pascal Richter, Erika Ábrahám)
  6. Lars Fischer, “Multi-step layout optimization of heliostat fields in central receiver systems” (Bachelor thesis, supervision: Pascal Richter, Erika Ábrahám)
  7. Menghze Hua, “Approximate model checking for probabilistic rectangular automata with continuous-time probability distributions on jumps” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
  8. Stefan Leachu,”Optimal building control using system linearization based on a generalized physics model” (Master thesis, supervision:  Erika Ábrahám, Ahmed Abida)
  9. Wei Lu, “Visualizing stochastic delay information for railway timetables”. (Master thesis, supervision: Erika Ábrahám)
  10. Laura-Sophie Kirchner,  “Automation and investigation of multi output machine learning control in buildings” (Master thesis, supervision: Ahmed Abida, Erika Ábrahám)
  11. Christoph von Oy, “Optimal design and scheduling of a smart city under uncertain renewable energy generation” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
  12. Viktor Panichkin, “Auralization and visualization of wind farms using augmented reality” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
  13. Marvin Thelen, “Quantification of uncertainties and determination of sensitivities for biogeochemical ocean simulations” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
  14. Aleksandar Timanov, “Visualization of the noise propagation in wind farms” (Bachelor thesis, supervision: Pascal Richter, Erika Ábrahám)
  15. Marvin Vogt, “Analysis of probabilistic hybrid automata in HyPro” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
  16. Paul Kobialka, “Connecting Simplex and Fourier-Motzkin into a novel quantifier elimination method for linear real algebra” (Master thesis, supervision: Erika Ábrahám, Jasper Nalbach)
  17. Lukas Wilke, “Probabilistic hyperproperties with rewards” (Bachelor thesis, supervision Erika Ábrahám)

2020

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

2019

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

2018

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

2017

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

2016

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

2015

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

2014

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

2013

  1. Matthias Ewert, “Modellierung des Radialverdichters eines PKW-Abgasturboladers” (Master thesis, supervision: Erika Ábrahám, Richard Aymanns, Dominik Lückmann)
  2. Kim Maren Haps, “Datatypes and tools for the analysis of hybrid systems” (Bachelor thesis, supervision: Johanna Nellen, Erika Ábrahám, Jürgen Giesl)
  3. Georg Jenneßen, “Optimierung eines Heliostatsfeldes unter Einsatz eines genetischen Algorithmus” (Diploma thesis, supervision:Pascal Richter, Erika Ábrahám, Martin Frank)
  4. Gereon Kremer, “Isolating real roots using adaptable-precision interval arithmetic” (Master thesis, supervision: Ulrich Loup, Erika Ábrahám)
  5. Amith Belur Nagabushana, “Minimal critical subsystems for PCTL” (Master thesis, supervision: Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen)
  6. Thomas Osterland, “Memory- and time-related action qualifiers in HSFCs” (Bachelor thesis, supervision: Johanna Nellen, Erika Ábrahám, Stefan Kowalewski)
  7. Henrik Schmitz, “Parallel user-defined strategies for QFNRA” (Diploma thesis, supervision: Erika Ábrahám, Florian Corzilius)
  8. Stefan Schupp,  “Interval constraint propagation in SMT-compliant decision procedures” (Master thesis, supervision: Erika Ábrahám, Florian Corzilius, Ulrich Loup)
  9. Marian Van de Veire, “Minimal critical subsystems for probabilistic models with nondeterminism” (Diploma thesis, supervision: Erika Ábrahám, Nils Jansen, Joost-Pieter Katoen)
  10. Andreas Vorpahl, “Compositional counterexamples for MDPs” (Master thesis, supervision: Nils Jansen, Erika Ábrahám, Joost-Pieter Katoen)

2012

  1. Kai Driessen, “Counterexample-guided abstraction refinement for hybrid SFC verification” (Bachelor thesis, supervision: Erika Ábrahám, Johanna Nellen)
  2. Alin Ionascu, “Modeling and controler synthesis of hybrid propulsion systems using artificial intelligence” (Master thesis, supervision: Erika Ábrahám, Johanna Nellen, Ulrich Loup)
  3. Sebastian Junges, “On Gröbner bases in SMT-compliant decision procedures” (Bachelor thesis, supervision:Erika Ábrahám, Ulrich Loup).
  4. Canan Kasaci, “Model-based resource monitoring and optimization” (Master thesis, supervision: Erika Ábrahám, Stefan Kowalewski, ASML)
  5. Joachim Redies, “An extension of the GiNaCRA library for the cylindrical algebraic decomposition” (Bachelor thesis, supervision: Erika Ábrahám, Ulrich Loup, Peter Rossmanith)
  6. Maik Scheffler, “Hierarchical counterexamples for DTMCs – Case studies” (Diploma thesis, supervision: Erika Ábrahám, Nils Jansen)
  7. Dennis Scully, “Preprocessing for solving non-linear real-arithmetic formulas” (Bachelor thesis, supervision: Erika Ábrahám, Florian Corzilius)
  8. Matthias Volk, “Verification and synthesis for parametric Markov chains” (Bachelor thesis, supervision: Erika Ábrahám, Nils Jansen, Florian Corzilius)

2011

  1. Florian Corzilius, “Virtual substitution in SMT solving” (Diploma thesis, supervision: Erika Ábrahám, Ulrich Loup)

2009

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