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

  • Implementing an ordered nullification-avoiding polynomial evaluation for CAD (contact: Gereon Kremer)
  • Non-linear optimization in SAT-modulo-theories solving (contact: Gereon Kremer)
  • Using machine learning techniques for strategy selection and synthesis (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)
  • 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.

  • Igor Bongartz, “Explaining plan infeasibility with UNSAT cores(Master Thesis,supervision: Erika Ábrahám, Francesco Leofante)
  • 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)
  • Henri Lotze, “Automated optimization in production planning” (Master thesis, supervision: Erika Ábrahám, Gereon Kremer)
  • Christopher Lösbrock, “Solving difference logic” (Bachelor thesis, supervision: Erika Ábrahám, Gereon Kremer, Matthias Volk)
  • Malte Neuß, “Implementation of OneCell CAD for nonlinear explanations” (Master thesis, supervision: Gereon Kremer)
  • Thomas Lange, “Anytime planning with Optimization Modulo Theories” (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)
  • Ömer Sali, “Solving non-linear problems using linearization techniques” (Master thesis, supervision: Gereon Kremer)
  • Lyudmila Vatskicheva, “Using simulation for counterexample validation in hybrid systems reachability analysis” (Bachelor thesis, supervision: Erika Ábrahám, Stefan Schupp)
  • Tobias Vogel, “Reachability analysis for compositional hybrid systems” (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

2017

2016

2015

2014

2013

2012

2011

2009