A list of example programs and case studies verified by the VerCors verification toolset
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.
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.
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.
| ID | Title | Verification features | Example source | Language | More information |
|---|---|---|---|---|---|
| 56 | Counting test | Arrays, Sequences, Summation patterns | Java | more info | |
| 50 | Domain of option types | Option types | Silver | more info | |
| 49 | Domain of lists | Lists | Silver | more info | |
| 48 | Domain of floats | Floats, Sequences | Silver | more info | |
| 45 | Overloading in Java | Java | more info | ||
| 44 | Annotating function declarations in C | OpenMP for C | more info | ||
| 43 | Submatrix clearing | Arrays, Iteration contracts, Matrices | OpenMP for C | more info | |
| 42 | Array clearing in C (succeeding) | Arrays, Iteration contracts | OpenMP for C | more info | |
| 41 | Array clearing kernel | Arrays, GPU Kernels | PVL | more info | |
| 40 | Summation reduction | Arrays, Floats, Iteration contracts, Sequences, Summation patterns | OpenMP for C | more info | |
| 39 | Summation kernel (version 2) | Arrays, Atomics, Barriers, GPU Kernels, Iteration contracts, Loop parallelisations | PVL | more info | |
| 38 | Summation kernel (version 1) | Arrays, GPU Kernels, Iteration contracts | PVL | more info | |
| 37 | Histogram submatrix | Arrays, Iteration contracts, Matrices | OpenMP for C | more info | |
| 36 | Histogram matrix | Arrays, Iteration contracts, Matrices | OpenMP for C | more info | |
| 35 | Forward dependencies (succeeding) | Arrays, Iteration contracts, Loop parallelisations | OpenMP for C | more info | |
| 34 | Kernel with host code | Arrays, Barriers, GPU Kernels, Loop parallelisations | PVL | more info | |
| 33 | Matrix accessing | Matrices | OpenMP for C | more info | |
| 32 | Array clearing (succeeding) | Arrays, Iteration contracts | Java | more info | |
| 30 | Basic contracts | OpenMP for C | more info | ||
| 29 | Postfix unary operators | PVL | more info |