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

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