Skip to Content

Concurrent Program Verification

Posted on

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. As of September 2017, I am involved in both as a postdoctoral researcher at the University of Twente.