Concurrent Program Verification
Programming languages like Java, that are recognised as striking a good balance between being easy to write and learn, and good for writing efficient code, can be improved by adding verification capabilities. This is the aim of projects like Key and OpenJML, but often the ability to write concurrent code needs to be sacrificed for being able to verify it. The Vercors tool offers verification for concurrent programs, and the Mercedes project aims to find game-changing methods for applying verification to concurrent programs. I started out as a postdoctoral researcher at the University of Twente on both projects. As of September 2018, I am an assistant professor there, still working on the VerCors and Mercedes projects.
Relevant publications include: