Theses

Available topics

Hybrid systems verification

  • Optimizing dynamic search strategies for hybrid automata reachability analysis algorithms (contact: Stefan Schupp)
  • Zeno-behavior in hybrid systems reachability analysis (contact: Stefan Schupp)
  • Conditional path refinement in hybrid systems reachability analysis (contact: Stefan Schupp)
  • Safety analysis for probabilistic hybrid systems (contact: Erika Abraham)
  • The implementation and evaluation of different reachability analysis algorithms using the HyPro toolbox (contact: Stefan Schupp)

SMT solving

  • Developing, implementing and evaluating different variable ordering heuristics for arithmetic theory decision procedures in SMT solving (contact: Erika Abraham)
  • Non-linear optimization in SAT-modulo-theories solving (contact: Gereon Kremer)
  • Solving uninterpreted functions within the Model Constructing Satisfiability Calculus (contact: Gereon Kremer)
  • 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

  • Probabilistic model repair for safe robot control (contact: Erika Abraham)
  • Probabilistic modeling of robot fleets in production logistics scenarios (contact: Erika Abraham)
  • Safety analysis for probabilistic hybrid systems (contact: Erika Abraham)

Miscellaneous

In progress

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

  1. Hanna Franzen, “Locally model based CAD for SMT solving” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
  2. Stella Coumbassa, “Optimal storage strategy for solar tower power plants” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
  3. Julian Düstersiek, “Probabilistic optimization of offshore wind farms” (Bachelor thesis, supervision: Pascal Richter, Erika Ábrahám)
  4. Aklima Zaman, “Linearization for SAT modulo real arithmetic solving” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
  5. Niklas Kotowski, “Application of Formal Methods in Autonomous Vehicle Control” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
  6. Daniel Cloerkes, “Reachability Analysis of Compositional Hybrid Systems” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
  7. Marta Grobelna, “Integration of Hybrid Systems Verification Methods in Matlab” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)

Completed

2019

  1. Karim Josef Abou Zeid, “Letterplace Gröbner bases, their implementation and applications” (Bachelor thesis, supervision: Erika Ábrahám, Viktor Levandovskyy)
  2. Linus Franke, “Modelling and optimization of large scale solar tower power plants” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
  3. Marwa Maghnie, “Simulation and optimization of offshore wind farms” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
  4. Leon Rabanus, “Probabilistic modeling of robot fleets in production logistics scenarios” (Bachelor thesis, supervision: Erika Ábrahám, Francesco Leofante)
  5. 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)