PhD student position in formal verification, Delft (The Netherlands)

The Programming Languages group at Delft University of Technology is looking for a fully-funded PhD student (4 years) on formal verification.

The successful candidate will will be enrolled in the TU Delft Graduate School and work under the supervision of Robbert Krebbers (daily supervisor) and Eelco Visser (promotor). The candidate will work on developing next-generation formal verification techniques and tools for programming concepts that so far have received relatively little attention, such as multilinguial software, (asynchronous) input/output, and non-functional properties. This work will revolve around Iris, a higher-order concurrency separation logic framework that is implemented in the Coq proof assistant. The exact research direction which will be determined based on the common interests of the candidate and the supervisor.