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)
• Reachability analysis for compositional hybrid systems (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)
• 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

• Implementation of a cloud application (PDF Implementation of a cloud application, contact: Pascal Richter)

In progress

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

• Jens Doveren, “Non-linear optimization in SAT-modulo-theories solving” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Hanna Franzen, “Locally model based CAD for SMT solving” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Stella Coumbassa, “Optimal storage strategy for solar tower power plants” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
• Julian Düstersiek, “Probabilistic optimization of offshore wind farms” (Bachelor thesis, supervision: Pascal Richter, Erika Ábrahám)
• Marwa Maghnie, “Simulation and optimization of offshore wind farms” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
• Linus Franke, “Simulation and optimization of solar tower power plants” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
• Igor Bongartz, “Explaining unsolvable planning tasks with unsatisfiable cores” (Master Thesis,supervision: Erika Ábrahám, Francesco Leofante)
• Leon Rabanus, “Probabilistic modeling of robot fleets in production logistics scenarios” (Bachelor thesis, supervision: Erika Ábrahám, Francesco Leofante)
• Lyudmila Vatskicheva, “Using simulation for counterexample validation in hybrid systems reachability analysis” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
• Aklima Zaman, “Linearization for SAT modulo real arithmetic solving” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)

Completed

2018

• Tom Neuhäuser, “Quantifier elimination by cylindrical algebraic decomposition” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Henri Lotze, “Automated optimization in production planning” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Malte Neuß, “Implementation of OneCell CAD for nonlinear explanations” (Master thesis, supervision: Gereon Kremer)
• Lorena Calvo Bartolomé, “Using Fourier-Motzkin variable elimination for MCSAT explanations in SMT-RAT” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Rebecca Haehn, “Using equational constraints in an incremental CAD projection” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Jan Hafer, “Using eigenvaluedecomposition for decoupling of dynamical systems” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
• Sabrina Kielmann, “Classifying current reachability analysis tools for hybrid systems” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
• Christopher Lösbrock, “Implementing an Incremental Solver for Difference Logic” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer, Matthias Volk)
• Ömer Sali, “Solving non-linear problems using linearization techniques” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Georg Wicke, “Optimization of aiming strategies for heliostats in solar-thermal power plants” (Bachelor thesis, supervision: Erika Ábrahám, Pascal Richter)
• Justin Winkens, “Dynamic reachability analysis for hybrid systems” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)

2017

• Roni Cakar, “Uncertainty quantification of wind farm models” (Bachelor thesis, supervision: Erika Ábrahám, Pascal Richter)
• Marta Grobelna, “SAT-modulo-theories solving for pseudo-Boolean constraints“. (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Wanja Hentze, “Infeasible subsets for nonlinear SMT” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Leonard Korp, “SMT-based planning for autonomous robot fleets”. (Bachelor thesis, supervision: Erika Ábrahám, Francesco Leofante, Gereon Kremer)
• Jasper Nalbach, “Embedding the virtual substitution in the MCSAT framework” (Bachelor thesis, supervision: Erika Ábrahám)
• Lukas Netz, “Genetic algorithms in renewable energy” (Master thesis, 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, supervision: Erika Ábrahám, Stefan Schupp)
• Phillip Florian, “Optimizing reachabiliy analysis for non-autonomous systems using ellipsoids” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
• Simon Froitzheim, “Efficient conversion of geometric state set representations for hybrid systems” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
• Levin Gerdes, “Generation of probabilistic models for solar thermal power plants” (Master thesis, supervision: Erika Ábrahám, Martin Frank)
• Rebecca Haehn, “Learning control strategies for hybrid vehicles using neural networks” (Bachelor thesis, supervision: Erika Ábrahám, Johanna Nellen)
• Dustin Hütter, “Adaptive dynamic reachability analysis for linear hybrid automata” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
• Johannes Neuhaus, “Development of a modular approach for hybrid systems reachability analysis” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
• Tarik Viehmann, “Projection operators for the CAD” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Patricia Wessel, “Grid-based control strategy for hybrid vehicles” (Bachelor thesis, supervision: Erika Ábrahám, Johanna Nellen)
• Tobias Winkler, “Using Thom’s Lemma for real algebraic numbers in the CAD” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)

2015

• Andreas Krüger, “Bitvectors in SMT-RAT and their application to integer arithmetics” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
• Lukas Netz, “Using Horner schemes to improve the efficiency and precision of interval constraint propagation” (Bachelor thesis, additional advisor: Florian Corzilius, Stefan Schupp)
• 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)
• Matthias Volk, “Using SAT solvers for industrial combinatorial problems” (Master thesis, supervision: Erika Ábrahám, Florian Corzilius)

2014

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

2013

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

2012

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

2011

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

2009

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