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 41-60 of 139 items.
IDTitleVerification featuresExample sourceLanguageMore information
 
83History-based reasoning: verifying a queueAtomics, Histories, SequencesJavamore info
102Incrementing in OpenCLArrays, GPU KernelsOpenCL (kernels)more info
93Induction lemma (succeeding)SequencesPVLmore info
99Input/output parameters (succeeding)PVLmore info
117Invariants and atomicsAtomics, Statically-scoped lockingPVLmore info
76Java threadingFork/join concurrency, WitnessesJavamore info
34Kernel with host codeArrays, Barriers, GPU Kernels, Loop parallelisationsPVLmore info
80Layered verification approachArrays, HistoriesJavamore info
84Linked listLists, SequencesPVLmore info
95Linked list propertiesLists, SequencesPVLmore info
158Longest common prefixArrays, Loop invariants, Quantified permissionsVerifyThis competition 2012PVLmore info
96Loop invariantsLoop invariantsPVLmore info
33Matrix accessingMatricesOpenMP for Cmore info
1Matrix transposeArrays, Iteration contracts, MatricesPVLmore info
63Model-abstraction permissionsFuturesPVLmore info
64Model-based reasoning: concurrent counting Futures, Statically-scoped locking, Statically-scoped parallelismPVLmore info
65Model-based reasoning: generalised concurrent counting Fork/join concurrency, Futures, Statically-scoped lockingPVLmore info
66Model-based reasoning: locking protocolAtomics, FuturesPVLmore info
67Model-based reasoning: unequal countingFork/join concurrency, Statically-scoped locking, Statically-scoped parallelismPVLmore info
60No-send-after-readFuturesJavamore info