Offered topics for theses
Hybrid systems verification
- Optimizing dynamic search strategies for hybrid automata reachability analysis algorithms (contact: Stefan Schupp)
- Exploiting parallelism in hybrid automata 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
- Solving non-linear problems using linearization techniques (contact: Gereon Kremer)
- Implementing an ordered nullification-avoiding polynomial evaluation for CAD (contact: Gereon Kremer)
- Enhancing CAD by equational constraints (contact: Gereon Kremer)
- Employing CAD for general purpose quantifier elimination (contact: Gereon Kremer)
- 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)
- Connecting Maple and SMT-RAT to join the strengths of computer algebra systems and SMT solving (contact: Gereon Kremer)
- SAT-modulo-theories solving for pseudo-Boolean constraints. (contact: Gereon Kremer)
- Solving Difference Logic (contact: Gereon Kremer)
- Solving constraint problems with SMT solvers (contact: Gereon Kremer)
- Breaking symmetries in SAT-modulo-theories formulas (contact: Gereon Kremer)
- Non-linear optimization in SAT-modulo-theories solving (contact: Gereon Kremer)
- Developing and implementing a satisfiability-equivalent transformation approach from the MiniZinc specification language into the SMT-LIB2 standard input format (contact: Gereon Kremer)
- 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)
- Safety verification for Simulink models (contact: Johanna Nellen)
- Encoding of linear temporal logic formulas by Simulink models (contact: Johanna Nellen)
In progress
Please ask your supervisor for our checklist with information for thesis students.
- Sabrina Kielmann, “Classifying current reachability analysis tools for hybrid systems” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
- Christopher Lösbrock, “Solving Difference Logic” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer, Matthias Volk)
- Jakob Gelhard, “Connecting Maple and SMT-RAT to join the strengths of computer algebra systems and SMT solving” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
- Jan Hafer, “Using eigenvaluedecomposition for decoupling of dynamical systems” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
Completed
2017
- Wanja Hentze, “Infeasible subsets for nonlinear SMT” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer)
- Jasper Nalbach, “Embedding the virtual substitution in the MCSAT framework” (Bachelor thesis, supervision: Erika Ábrahám)
- Marta Grobelna, “SAT-modulo-theories solving for pseudo-Boolean constraints“. (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)
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: 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
- Alin Ionascu, “Modeling and controler synthesis of hybrid propulsion systems using artificial intelligence” (Master thesis, supervision: Erika Ábrahám, Johanna Nellen, Ulrich Loup)
- Kai Driessen, “Counterexample-guided abstraction refinement for hybrid SFC verification” (Bachelor thesis, supervision: Erika Ábrahám, Johanna Nellen)
- Dennis Scully, “Preprocessing for solving non-linear real-arithmetic formulas” (Bachelor thesis, supervision: Erika Ábrahám, Florian Corzilius)
- Sebastian Junges, “On Gröbner bases in SMT-compliant decision procedures” (Bachelor thesis, supervision:Erika Ábrahám, Ulrich Loup).
- Matthias Volk, “Verification and synthesis for parametric Markov chains” (Bachelor thesis, supervision: Erika Ábrahám, Nils Jansen, Florian Corzilius)
- Joachim Redies, “An extension of the GiNaCRA library for the cylindrical algebraic decomposition” (Bachelor thesis, supervision: Erika Ábrahám, Ulrich Loup, Peter Rossmanith)
- Canan Kasaci, “Model-based resource monitoring and optimization” (Master thesis, supervision:Erika Ábrahám, Stefan Kowalewski, ASML)
- Maik Scheffler, “Hierarchical counterexamples for DTMCs – Case studies” (Diploma thesis, supervision: Erika Ábrahám, Nils Jansen)
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)