VerCors Example Database

A list of example programs and case studies verified by the VerCors verification toolset

About VerCors

VerCors is a toolset for practical mechanised verification of parallel and concurrent software under different concurrency models, notably heterogeneous and homogeneous threading. VerCors has verification support for multiple languages with concurrency features, such as Java, OpenCL (i.e. GPU kernels and atomics), and OpenMP for C (i.e. compiler directives). VerCors uses separation logic with permission accounting as its logical foundation.

Try online »


The source code of VerCors is publicly available and can be downloaded from Github. Installation instructions and example verification cases are also provided. VerCors has been tested on Linux, MacOS X, and on Windows (via Cygwin). Limited documentation of the annotation language is provided at the Github Wiki.

Download VerCors »


For questions and (technical) support, email to "w.h.m.oortwijn at utwente dot nl". Bug reports and feature requests can be submitted via the issue tracker on Github. A complete list of papers related to the VerCors project is given here.

Contact us »

Example database

Showing 1-20 of 139 items.
IDTitleVerification featuresExample sourceLanguageMore information
48Domain of floatsFloats, SequencesSilvermore info
49Domain of listsListsSilvermore info
50Domain of option typesOption typesSilvermore info
1Matrix transposeArrays, Iteration contracts, MatricesPVLmore info
4Parallel prefix sumArrays, Barriers, GPU Kernels, MatricesPVLmore info
9Forward dependencies (kernel 1)Arrays, Barriers, GPU KernelsPVLmore info
10Forward dependencies (kernel 2)Arrays, Barriers, GPU KernelsPVLmore info
12PVL kernel (version 2)Arrays, Barriers, GPU KernelsPVLmore info
13PVL kernel (version 3)Arrays, Barriers, GPU KernelsPVLmore info
14PVL kernel (version 1)Arrays, Barriers, GPU KernelsPVLmore info
15Vector additionArrays, Barriers, GPU KernelsPVLmore info
29Postfix unary operatorsPVLmore info
34Kernel with host codeArrays, Barriers, GPU Kernels, Loop parallelisationsPVLmore info
38Summation kernel (version 1)Arrays, GPU Kernels, Iteration contractsPVLmore info
39Summation kernel (version 2)Arrays, Atomics, Barriers, GPU Kernels, Iteration contracts, Loop parallelisationsPVLmore info
41Array clearing kernelArrays, GPU KernelsPVLmore info
59Fork/join updatesFork/join concurrencyPVLmore info
61Parallel GCDFutures, Statically-scoped locking, Statically-scoped parallelismVerifyThis competition 2015PVLmore info
62Simple model abstractionFuturesPVLmore info
63Model-abstraction permissionsFuturesPVLmore info