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
179ColoredTilesArrays, Iteration contracts, Loop invariants, Quantified permissions, SequencesVerifyThis competition 2018PVLmore info
178GapBufferArrays, Loop invariants, SequencesVerifyThis competition 2018PVLmore info
1772Iteration contractsJavamore info
176Witnesses: PredicatesWitnessesJavamore info
174Witnesses: Magic wand (Silver)Loop invariants, Magic wandsJavamore info
173Witnesses: Magic wandLoop invariants, Magic wands, WitnessesJavamore info
172Witnesses: TwiceJavamore info
171Witnesses: Recursive tree 3 (magic wand)Magic wands, Sequences, Trees, WitnessesJavamore info
168Recursive trees: Deleting smallest elementSequences, TreesJavamore info
167Witnesses: RosterWitnessesJavamore info
166Witnesses: List iteratorLists, Loop invariants, Magic wands, WitnessesJavamore info
165Witnesses: List appending (inline)Lists, SequencesJavamore info
164Witnesses: List appending (out-of-sync)Lists, SequencesJavamore info
163Witnesses: List appending (magic wand)Lists, Magic wands, Sequences, WitnessesJavamore info
162Witnesses: GettersWitnessesJavamore info
161Witnesses: CounterStateLoop invariants, WitnessesJavamore info
160Verifying wait-notify patternsFork/join concurrency, Locking, Loop invariantsPVLmore info
159Relaxed prefixLoop invariants, Quantified permissionsVerifyThis competition 2015PVLmore info
158Longest common prefixArrays, Loop invariants, Quantified permissionsVerifyThis competition 2012PVLmore info
157Using \instanceof and \typeofJavamore info