Vacancies

A PhD position in the topic Higher-order Term Rewriting for Program Equivalence. The position is for four years, and comes with a competitive salary and very attractive employment conditions. Interested students who either already hold a Masters' degree in computer science, mathematics, or a related area, or who will complete such a degree before September, are encouraged to apply. The initial application deadline is 20 June, but will be extended if no suitable candidate is found by that time. As a PhD candidate, you will conduct research into higher-order term rewriting systems with logical constraints. This project brings together two different areas of theoretical computer science: higher-order term rewriting and program equivalence analysis. Term rewriting is a formal system that can be used to specify algorithms. Its simple, rigorous definition makes it very suitable for formal analysis, and as a result, its properties are well studied. Higher-order term rewriting extends standard term rewriting with anonymous functions and binders as in the lambda-calculus, thus providing a highly liberal class of systems. Term rewriting can be combined with a logical theory and logical constraints; for example, integer numbers and conditions such as x >= 1 /\ y != x. With this approach, it is possible to model programs in common programming languages; higher-order term rewriting systems in particular offer a natural model to analyse functional and object-oriented programming languages. Program equivalence analysis is the study of whether two systems of program code have the same result, given the same input. This is a challenging field with many applications both in business practice and in other areas of computing science. In this project, your task will be to develop techniques for program equivalence analysis, by analysing in particular higher-order term rewriting systems with logical constraints, which encode realistic programs. The majority of the project is the development of theory, but since it is a goal to develop automatable techniques, you will also implement some of your techniques in a prototype analysis tool. You will be supervised by Dr Cynthia Kop. If you wish to learn more, feel free to send an e-mail to C.Kop@cs.ru.nl.
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.
A PhD position within the TTW Mascot project on Testing in Times of Continuous Change (TicToc). Contact Jan Tretmans if you are interested.

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!