The VerCors project
Afshin Amighi, Stefan Blom, Marieke Huisman, Marina Zaharieva-Stojanovski · 2012
This paper describes the first results and on-going work in the VerCors project. The VerCors project is about Verification of Concurrent Data Structures. Its goal is to develop a specification language and program logic for concurrent programs, and in particular for concurrent data structures, as these are the essential building blocks of many different concurrent programs. The program logic is based on our earlier work on permission-based separation logic for Java. This is an extension of Hoare logic that is particularly convenient to reason about concurrent programs.