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 |
|---|---|---|---|---|---|
| 126 | Permissions: Long swapping | Java | more info | ||
| 125 | Permissions: Integer swapping | Java | more info | ||
| 124 | Permissions: Roster (fixed) | Lists | Java | more info | |
| 123 | Permissions: multi-increment | Loop invariants | Java | more info | |
| 122 | Single-threaded incrementing | Loop invariants | Java | more info | |
| 121 | Single-threaded counting | Loop invariants | Java | more info | |
| 120 | Permissions: Bad loop (failing case 2) | Loop invariants | Java | more info | |
| 119 | Permissions: Bad loop (failing case 1) | Loop invariants | Java | more info | |
| 118 | Parallel Block: Blanking | Arrays, Iteration contracts, Matrices, Quantified permissions, Statically-scoped parallelism | PVL | more info | |
| 117 | Invariants and atomics | Atomics, Statically-scoped locking | PVL | more info | |
| 116 | Block parallelism | Iteration contracts, Loop parallelisations, Statically-scoped parallelism | PVL | more info | |
| 115 | Barrier with atomics | Arrays, Atomics, Barriers, Loop parallelisations, Quantified permissions, Statically-scoped locking, Statically-scoped parallelism | PVL | more info | |
| 114 | OpenMP: Array blanking | Arrays, Iteration contracts, Pragmas, Quantified permissions | OpenMP for C | more info | |
| 112 | OpenMP: Parallel sections (succeeding) | Arrays, Iteration contracts, Loop parallelisations, Pragmas, Quantified permissions | OpenMP for C | more info | |
| 110 | OpenMP: Vector addition (single) | Arrays, Loop vectorisation, Quantified permissions | PVL | more info | |
| 109 | Statically-scoped parallelism | Arrays, Iteration contracts, Quantified permissions, Statically-scoped parallelism | PVL | more info | |
| 107 | OpenMP: Array copying | Arrays, Iteration contracts, Loop parallelisations, Pragmas, Quantified permissions | OpenMP for C | more info | |
| 106 | OpenMP: SIMD translation | Arrays, Iteration contracts, Loop parallelisations, Loop vectorisation, Quantified permissions | PVL | more info | |
| 105 | OpenMP: Vector addition (PVL) | Arrays, Loop vectorisation, Quantified permissions | PVL | more info | |
| 104 | OpenMP: Loop fusion | Arrays, Iteration contracts, Pragmas, Quantified permissions | OpenMP for C | more info |