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 101-120 of 139 items.
IDTitleVerification featuresExample sourceLanguageMore information
128Permissions: BoxingPVLmore info
129Predicates: Linked integer listListsJavamore info
130Predicates: Tree traversalSequences, TreesJavamore info
131Predicates: Min-max listListsJavamore info
132Refute: require falseJavamore info
133Refute: unsatisfiableJavamore info
134Refute: bad framingPVLmore info
135Refute: refuting (case 1)Javamore info
136Refute: refuting (case 2)Javamore info
137Refute: refuting (case 3)Javamore info
138Refute: refuting (case 4)Javamore info
139Refute: refuting (case 5)Javamore info
148Synchronisers: CountDownLatchAtomics, Loop invariants, WitnessesJavamore info
149Synchronisers: ReentrantLockAtomics, Locking, Loop invariants, WitnessesJavamore info
150Synchronisers: SemaphoreAtomics, Loop invariants, WitnessesJavamore info
153Fork/join incrementing (succeeding)Fork/join concurrencyJavamore info
154Fork/join incrementing (failing 1)Fork/join concurrencyJavamore info
155Fork/join incrementing (failing 2)Fork/join concurrencyJavamore info
156Type castingTreesJavamore info
157Using \instanceof and \typeofJavamore info