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
- 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.
- 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)
- 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)
- Niklas Kotowski, “Application of Formal Methods in Autonomous Vehicle Control” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
- Daniel Cloerkes, “Reachability Analysis of Compositional Hybrid Systems” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
- Marta Grobelna, “Integration of Hybrid Systems Verification Methods in Matlab” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
Completed
2018
- Lorena Calvo Bartolomé, “Using Fourier-Motzkin variable elimination for MCSAT explanations in SMT-RAT” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
- Igor Bongartz, “Explaining unsolvable planning tasks with unsatisfiable cores” (Master Thesis,supervision: Erika Ábrahám, Francesco Leofante)
- Linus Franke, “Modelling and optimization of large scale solar tower power plants” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
- Jan Hafer, “Using eigenvalue decomposition in hybrid systems reachability analysis” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
- Rebecca Haehn, “Using equational constraints in an incremental CAD projection” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
- Sabrina Kielmann, “Comparing the expressivity and usabiliy of hybrid systems’ modeling languages” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
- Henri Lotze, “Automated optimization in production planning” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
- Christopher Lösbrock, “Implementing an incremental solver for difference logic” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer, Matthias Volk)
- Tom Neuhäuser, “Quantifier elimination by cylindrical algebraic decomposition” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
- Malte Neuß, “Using single CAD cells as explanations in MCSAT-style SMT solving” (Master thesis, supervision: Gereon Kremer)
- Leon Rabanus, “Probabilistic modeling of robot fleets in production logistics scenarios” (Bachelor thesis, supervision: Erika Ábrahám, Francesco Leofante)
- Ömer Sali, “Linearization techniques for nonlinear arithmetic problems in SMT” (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, “Context-dependent reachability analysis for hybrid automata” (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, “Solving pseudo-Boolean constraints“. (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
- Wanja Hentze, “Computing minimal infeasible subsets for the cylindrical algebraic decomposition” (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, “Analysis on discretization of gene parameters in evolutionary algorithms” (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, “Comparing different projection operators in the cylindrical algebraic decomposition for SMT solving” (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 encodings for real algebraic numbers in the cylindrical algebraic decomposition” (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, “Optimierung eines Heliostatsfeldes unter Einsatz eines genetischen Algorithmus” (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)