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
 
114OpenMP: Array blankingArrays, Iteration contracts, Pragmas, Quantified permissionsOpenMP for Cmore info
107OpenMP: Array copyingArrays, Iteration contracts, Loop parallelisations, Pragmas, Quantified permissionsOpenMP for Cmore info
104OpenMP: Loop fusionArrays, Iteration contracts, Pragmas, Quantified permissionsOpenMP for Cmore info
112OpenMP: Parallel sections (succeeding)Arrays, Iteration contracts, Loop parallelisations, Pragmas, Quantified permissionsOpenMP for Cmore info
103OpenMP: SIMD programsArrays, Iteration contracts, Loop parallelisations, Pragmas, Quantified permissionsOpenMP for Cmore info
106OpenMP: SIMD translationArrays, Iteration contracts, Loop parallelisations, Loop vectorisation, Quantified permissionsPVLmore info
105OpenMP: Vector addition (PVL)Arrays, Loop vectorisation, Quantified permissionsPVLmore info
110OpenMP: Vector addition (single)Arrays, Loop vectorisation, Quantified permissionsPVLmore info
97Option typesOption typesPVLmore info
45Overloading in JavaJavamore info
87Owicki-GriesFork/join concurrency, LockingPVLmore info
118Parallel Block: BlankingArrays, Iteration contracts, Matrices, Quantified permissions, Statically-scoped parallelismPVLmore info
75Parallel FibonacciFork/join concurrency, WitnessesJavamore info
90Parallel Fibonacci (PVL)Fork/join concurrencyPVLmore info
61Parallel GCDFutures, Statically-scoped locking, Statically-scoped parallelismVerifyThis competition 2015PVLmore info
4Parallel prefix sumArrays, Barriers, GPU Kernels, MatricesPVLmore info
119Permissions: Bad loop (failing case 1)Loop invariantsJavamore info
120Permissions: Bad loop (failing case 2)Loop invariantsJavamore info
127Permissions: Binary search treeLoop invariants, Stacks, TreesJavamore info
128Permissions: BoxingPVLmore info