print · source · login   


  • We are looking for a highly motivated PhD candidate to join our project on the formal model-based analysis of partially observable Markov models. Your main responsibilities will be to conduct cutting-edge research leading to the development of faster and more scalable techniques for the analysis of safety-critical systems that operate based on limited information about their environment. The project allows to freely explore connections between runtime verification, model checking, automata learning and reinforcement learning, depending of the joint interests of the principal investigator and you. While previous knowledge in model checking, Markov decision processes or automata theory, and programming skills in C++ or Python are beneficial, the willingness to learn and extend your knowledge in these areas is more crucial. We offer joining a fun and diverse group that maintains a range of international cooperations. In 2021, we published our research in top conferences such as CAV, TACAS, (formal methods) AAAI (artificial intelligence) and RSS (robotics). Furthermore, our group actively contributes to the development of the state-of-the-art probabilistic model checker Storm. Contact Sebastian Junges if you are interested.
  • A PhD position on program verification and Iris. The project involves the development of automatic methods for program verification based on concurrent separation logic and type systems. You will apply the developed methods to verify security and correctness properties of a realistic hypervisor written in C, as part of an ongoing collaborative project with Google, MPI-SWS, Cambridge, SNU, and Aarhus. Contact Robbert Krebbers if you are interested and look at the following page at his website:
  • A PhD position on at the intersection of semantics, category theory and coalgebra. As a PhD candidate on this project, you will conduct research at the intersection of semantics, category theory and coalgebra. Coalgebra is an elegant mathematical theory of state-based systems (transition systems, various kinds of automata, probabilistic models), based on category theory. In this context, distributive laws capture the interaction between coalgebra and algebra, and have shown to be very useful as a general way of modelling programming language semantics, as well as automata constructions and powerful co-inductive proof techniques. The aim of the project is to investigate distributive laws in their own right, and build a toolkit for constructing, combining and analysing them. You can build on several existing approaches, but will have plenty of freedom to define your own direction and focus. If you wish to learn more about the project, don't hesitate to get in touch via

We are always looking for motivated PhD candidates. Please contact one of us when you are interested in one of these projects/positions, or any other PhD project related to Software Science!