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
2Array zippingArrays, Iteration contracts, Loop parallelisationsJavamore info
17Atomic read/write witnessesAtomics, WitnessesJavamore info
18Deposit/withdraw lockAtomics, Locking, WitnessesJavamore info
19Single-entrant spin lockAtomics, Locking, WitnessesJavamore info
20Single producer/consumerAtomics, WitnessesJavamore info
21Simple hash table (with find-or-put)Atomics, WitnessesJavamore info
22Reentrant lockingAtomics, Locking, WitnessesJavamore info
23Single cellAtomics, WitnessesJavamore info
32Array clearing (succeeding)Arrays, Iteration contractsJavamore info
45Overloading in JavaJavamore info
56Counting testArrays, Sequences, Summation patternsJavamore info
57Float summationsArrays, Floats, Sequences, Summation patternsJavamore info
58Histogram with summationsArrays, Sequences, Summation patternsJavamore info
60No-send-after-readFuturesJavamore info
71History-based reasoning: incrementingHistoriesJavamore info
72History-based reasoning: correctness checking (Java)HistoriesJavamore info
73History-based reasoning: loopsHistoriesJavamore info
75Parallel FibonacciFork/join concurrency, WitnessesJavamore info
76Java threadingFork/join concurrency, WitnessesJavamore info
80Layered verification approachArrays, HistoriesJavamore info