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)

Computational Renewable Energy
Contact: Pascal Richter

Miscellaneous

• A Python framework for Optimal Planning Modulo Theories (description; contact: Erika Abraham, Francesco Leofante).

In progress

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

1. Daniel Cloerkes, “Reachability analysis of compositional hybrid systems” (Master thesis, supervision: Erika Ábrahám, Stefan Schupp)
2. Hanna Franzen, “Locally model based CAD for SMT solving” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
3. Florian Hövelmann, “Advanced raytracer for solar tower power plants” (Bachelor thesis, supervision: Pascal Richter, Erika Ábrahám)
4. Hang Khuat, “Efficient implementation of HyperPCTL model checking” (Master thesis, supervision: Erika Ábrahám)
5. Christian Kiricenko, “Developing a GUI for a hybrid systems reachability analysis tool” (Bachelor thesis, supervision Erika Ábrahám, Stefan Schupp)
6. Sergej Neuberger, “Safety verification and parameter synthesis for non-linear hybrid systems using Flow*” (Bachelor thesis, supervision Erika Ábrahám, Stefan Schupp)
7. Anton Stanchev, “TBA” (Bachelor thesis, supervision Erika Ábrahám, Rebecca Haehn)
8. Phillip Tse, “Template polyhedra in hybrid systems reachability analysis” (Master thesis, supervision Erika Ábrahám, Stefan Schupp)
9. Laurids Vollmann, “Parameter study of genetic algorithms for layout optimization in renewable energy power plants” (Master thesis, supervision: Pascal Richter, Erika Ábrahám)
10. Simeon Kalichkov, “TBA” (Bachelor thesis, supervision Erika Ábrahám, Rebecca Haehn)

Completed

2019

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

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)