Blogs (61) >>
Mon 16 Jul 2018 17:15 - 17:45 at Hanoi - Session 3

VerCors is a tool set that specialises in automated verification of parallel and concurrent programs, written in high-level languages like (subsets of) Java and C, annotated with JML-like contracts. VerCors is able to reason automatically about various concurrency constructs, including: (i) fork/join concurrency, as found in e.g. Java, (ii) GPU kernels with barriers and atomic operations in OpenCL, and (iii) compiler directives for automatic parallelisation in the context of OpenMP for C. The main goal of VerCors is to lift existing verification technology towards advanced concurrency constructs found in modern programming languages, rather than developing new verification technology from scratch. VerCors therefore translates input verification problems to the intermediate language of Viper —the back-end verifier of VerCors. VerCors allows to reason about data-race freedom, memory safety, and functional correctness of input programs.

This tool demonstration gives an overview of the various concurrency features that VerCors can reason about. We discuss the annotation language of VerCors, as well as its permission system, and demonstrate how this is used to reason about parallelism and concurrency

Mon 16 Jul (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:15: FTfJP - Session 3 at Hanoi
FTfJP-2018-papers16:00 - 16:25
David CokCEA, LIST, Software Safety and Security Laboratory
FTfJP-2018-papers16:25 - 16:50
Davide AnconaUniversity of Genova, Francesco DagninoDIBRIS, University of Genova, Italy, Luca FranceschiniDIBRIS, University of Genova
FTfJP-2018-papers16:50 - 17:15
Pascal WeisenburgerTechnische Universität Darmstadt, Tobias ReinhardTechnische Universität Darmstadt, Guido SalvaneschiTU Darmstadt
FTfJP-2018-papers17:15 - 17:45
Wytse OortwijnUniversity of Twente, The Netherlands
FTfJP-2018-papers17:45 - 18:15
Sebastiaan Joosten, Wytse OortwijnUniversity of Twente, The Netherlands, Mohsen SafariUniversity of Twente, The Netherlands, Marieke HuismanUniversity of Twente