Apr 29, 2014: Stefan Blom: The VerCors Tool for Verification of Concurrent Programs

April 29, 2014The VerCors Tool for Verification of Concurrent Programs
Room: HalB 2FStefan Blom
12:30-13:30

The VerCors tool implements thread-modular static verification of concurrent programs, annotated with functional properties and heap access permissions. The tool supports both generic multithreaded and vector-based programming models. In particular, it can verify multithreaded programs written in Java, specified with JML extended with separation logic. It can also verify parallelizable programs written in a toy language that supports the characteristic features of OpenCL. The tool verifies programs by first encoding the specified program into a much simpler programming language and then applying the Chalice verifier to the simplified program.

In this talk, we will give an overview of the architecture of the VerCors Tool, by means of a demo we will introduce its distinguishing features and we will give an overview of work-in-progress and future work.