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

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 18:15
Session 3FTfJP at Hanoi
16:00
25m
Short-paper
Reasoning about Functional Programming in Java and C++
FTfJP
David Cok CEA, LIST, Software Safety and Security Laboratory
Pre-print
16:25
25m
Short-paper
A Formalism for Specification of Java API Interfaces
FTfJP
Davide Ancona University of Genova, Francesco Dagnino DIBRIS, University of Genova, Italy, Luca Franceschini DIBRIS, University of Genova
Pre-print
16:50
25m
Short-paper
Static Latency Tracking with Placement Types
FTfJP
Pascal Weisenburger Technische Universität Darmstadt, Tobias Reinhard Technische Universität Darmstadt, Guido Salvaneschi TU Darmstadt
Pre-print
17:15
30m
Demonstration
Tool demonstration: The VerCors Verification Toolset
FTfJP
Wytse Oortwijn University of Twente, The Netherlands
Pre-print
17:45
30m
Full-paper
An Exercise in Verifying Sequential Programs with VerCors
FTfJP
Sebastiaan Joosten , Wytse Oortwijn University of Twente, The Netherlands, Mohsen Safari University of Twente, The Netherlands, Marieke Huisman University of Twente
Pre-print