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)
    • Enhancing CAD by equational constraints (contact: Gereon Kremer)
    • Solving Difference Logic (contact: Gereon Kremer)


  • Implementing an ordered nullification-avoiding polynomial evaluation for CAD (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 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)


In progress

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