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 »

Download

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 »

Contact

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 61-80 of 139 items.
IDTitleVerification featuresExample sourceLanguageMore information
 
171Witnesses: Recursive tree 3 (magic wand)Magic wands, Sequences, Trees, WitnessesJavamore info
172Witnesses: TwiceJavamore info
173Witnesses: Magic wandLoop invariants, Magic wands, WitnessesJavamore info
174Witnesses: Magic wand (Silver)Loop invariants, Magic wandsJavamore info
176Witnesses: PredicatesWitnessesJavamore info
1772Iteration contractsJavamore info
102Incrementing in OpenCLArrays, GPU KernelsOpenCL (kernels)more info
6Backward dependencies (error 1)Arrays, Iteration contracts, Loop parallelisationsOpenMP for Cmore info
7Basic C exampleArrays, Iteration contracts, Loop parallelisations, MatricesOpenMP for Cmore info
8Forward dependencies (error 1)Arrays, Iteration contracts, Loop parallelisationsOpenMP for Cmore info
30Basic contractsOpenMP for Cmore info
33Matrix accessingMatricesOpenMP for Cmore info
35Forward dependencies (succeeding)Arrays, Iteration contracts, Loop parallelisationsOpenMP for Cmore info
36Histogram matrixArrays, Iteration contracts, MatricesOpenMP for Cmore info
37Histogram submatrixArrays, Iteration contracts, MatricesOpenMP for Cmore info
40Summation reductionArrays, Floats, Iteration contracts, Sequences, Summation patternsOpenMP for Cmore info
42Array clearing in C (succeeding)Arrays, Iteration contractsOpenMP for Cmore info
43Submatrix clearingArrays, Iteration contracts, MatricesOpenMP for Cmore info
44Annotating function declarations in COpenMP for Cmore info
103OpenMP: SIMD programsArrays, Iteration contracts, Loop parallelisations, Pragmas, Quantified permissionsOpenMP for Cmore info