print · source · login   


  • 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!