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 |
|---|---|---|---|---|---|
| 156 | Type casting | Trees | Java | more info | |
| 155 | Fork/join incrementing (failing 2) | Fork/join concurrency | Java | more info | |
| 154 | Fork/join incrementing (failing 1) | Fork/join concurrency | Java | more info | |
| 153 | Fork/join incrementing (succeeding) | Fork/join concurrency | Java | more info | |
| 150 | Synchronisers: Semaphore | Atomics, Loop invariants, Witnesses | Java | more info | |
| 149 | Synchronisers: ReentrantLock | Atomics, Locking, Loop invariants, Witnesses | Java | more info | |
| 148 | Synchronisers: CountDownLatch | Atomics, Loop invariants, Witnesses | Java | more info | |
| 139 | Refute: refuting (case 5) | Java | more info | ||
| 138 | Refute: refuting (case 4) | Java | more info | ||
| 137 | Refute: refuting (case 3) | Java | more info | ||
| 136 | Refute: refuting (case 2) | Java | more info | ||
| 135 | Refute: refuting (case 1) | Java | more info | ||
| 134 | Refute: bad framing | PVL | more info | ||
| 133 | Refute: unsatisfiable | Java | more info | ||
| 132 | Refute: require false | Java | more info | ||
| 131 | Predicates: Min-max list | Lists | Java | more info | |
| 130 | Predicates: Tree traversal | Sequences, Trees | Java | more info | |
| 129 | Predicates: Linked integer list | Lists | Java | more info | |
| 128 | Permissions: Boxing | PVL | more info | ||
| 127 | Permissions: Binary search tree | Loop invariants, Stacks, Trees | Java | more info |