Example Database

Title Verification Features Language Verify
Matrix transpose Iteration contracts, Arrays, Matrices PVL
Array zipping Iteration contracts, Arrays, Loop parallelisations Java
Parallel prefix sum GPU Kernels, Arrays, Matrices, Barriers PVL
Backward dependencies (error 1) Iteration contracts, Arrays, Loop parallelisations C / OpenMP / OpenCL
Basic C example Iteration contracts, Arrays, Matrices, Loop parallelisations C / OpenMP / OpenCL
Forward dependencies (error 1) Iteration contracts, Arrays, Loop parallelisations C / OpenMP / OpenCL
Forward dependencies (kernel 1) GPU Kernels, Arrays, Barriers PVL
Forward dependencies (kernel 2) GPU Kernels, Arrays, Barriers PVL
PVL kernel (version 2) GPU Kernels, Arrays, Barriers PVL
PVL kernel (version 3) GPU Kernels, Arrays, Barriers PVL
PVL kernel (version 1) GPU Kernels, Arrays, Barriers PVL
Vector addition GPU Kernels, Arrays, Barriers PVL
Atomic read/write witnesses Atomics, Witnesses Java
Deposit/withdraw lock Atomics, Witnesses, Locking Java
Single-entrant spin lock Atomics, Witnesses, Locking Java
Single producer/consumer Atomics, Witnesses Java
Simple hash table (with find-or-put) Atomics, Witnesses Java
Reentrant locking Atomics, Witnesses, Locking Java
Single cell Atomics, Witnesses Java
Postfix unary operators PVL
Basic contracts C / OpenMP / OpenCL
Array clearing (succeeding) Iteration contracts, Arrays Java
Matrix accessing Matrices C / OpenMP / OpenCL
Kernel with host code GPU Kernels, Arrays, Barriers, Loop parallelisations PVL
Forward dependencies (succeeding) Iteration contracts, Arrays, Loop parallelisations C / OpenMP / OpenCL
Histogram matrix Iteration contracts, Arrays, Matrices C / OpenMP / OpenCL
Histogram submatrix Iteration contracts, Arrays, Matrices C / OpenMP / OpenCL
Summation kernel (version 1) GPU Kernels, Iteration contracts, Arrays PVL
Summation kernel (version 2) GPU Kernels, Iteration contracts, Arrays, Barriers, Loop parallelisations, Atomics PVL
Summation reduction Sequences, Iteration contracts, Arrays, Summation patterns, Floats C / OpenMP / OpenCL
Array clearing kernel GPU Kernels, Arrays PVL
Array clearing in C (succeeding) Iteration contracts, Arrays C / OpenMP / OpenCL
Submatrix clearing Iteration contracts, Arrays, Matrices C / OpenMP / OpenCL
Annotating function declarations in C C / OpenMP / OpenCL
Overloading in Java Java
Domain of floats Sequences, Floats Viper
Domain of lists Lists Viper
Domain of option types Option types Viper
Counting test Sequences, Arrays, Summation patterns Java
Float summations Sequences, Arrays, Summation patterns, Floats Java
Histogram with summations Sequences, Arrays, Summation patterns Java
Fork/join updates Fork/join concurrency PVL
No-send-after-read Futures Java
Parallel GCD Futures, Statically-scoped locking, Statically-scoped parallelism PVL
Simple model abstraction Futures PVL
Model-abstraction permissions Futures PVL
Model-based reasoning: concurrent counting Futures, Statically-scoped locking, Statically-scoped parallelism PVL
Model-based reasoning: generalised concurrent counting Fork/join concurrency, Futures, Statically-scoped locking PVL
Model-based reasoning: locking protocol Atomics, Futures PVL
Model-based reasoning: unequal counting Fork/join concurrency, Statically-scoped locking, Statically-scoped parallelism PVL
Verifying goto (failing) Goto PVL
Verifying goto (succeeding) Goto PVL
History-based reasoning: correctness checking (PVL) Histories PVL
History-based reasoning: incrementing (Java) Histories Java
History-based reasoning: correctness checking (Java) Histories Java
History-based reasoning: loops Histories Java
History-based reasoning: incrementing (PVL) Histories PVL
Parallel Fibonacci Witnesses, Fork/join concurrency Java
Java threading Witnesses, Fork/join concurrency Java
Function problem PVL
Layered verification approach Arrays, Histories Java
Verifying Java 6 Lock Arrays, Atomics, Locking Java
Verifying a queue Atomics, Lists Java
History-based reasoning: verifying a queue Sequences, Atomics, Histories Java
Linked list Sequences, Lists PVL
Owicki-Gries Locking, Fork/join concurrency PVL
Array properties Sequences, Arrays PVL
Exponentials Java
Parallel Fibonacci (PVL) Fork/join concurrency PVL
Functions and resources Java
Induction lemma (succeeding) Sequences PVL
Linked list properties Sequences, Lists PVL
Loop invariants Loop invariants PVL
Option types Option types PVL
Input/output parameters (succeeding) PVL
Witness encoding Witnesses PVL
Zero Array (PVL) Arrays, Loop invariants, Quantified permissions PVL
Incrementing in OpenCL GPU Kernels, Arrays Cuda
OpenMP: SIMD programs Iteration contracts, Arrays, Loop parallelisations, Quantified permissions, Pragmas C / OpenMP / OpenCL
OpenMP: Loop fusion Iteration contracts, Arrays, Quantified permissions, Pragmas C / OpenMP / OpenCL
OpenMP: Vector addition (PVL) Arrays, Quantified permissions, Loop vectorisation PVL
OpenMP: SIMD translation Iteration contracts, Arrays, Loop parallelisations, Quantified permissions, Loop vectorisation PVL
OpenMP: Array copying Iteration contracts, Arrays, Loop parallelisations, Quantified permissions, Pragmas C / OpenMP / OpenCL
Statically-scoped parallelism Iteration contracts, Arrays, Statically-scoped parallelism, Quantified permissions PVL
OpenMP: Vector addition (single) Arrays, Quantified permissions, Loop vectorisation PVL
OpenMP: Parallel sections (succeeding) Iteration contracts, Arrays, Loop parallelisations, Quantified permissions, Pragmas C / OpenMP / OpenCL
OpenMP: Array blanking Iteration contracts, Arrays, Quantified permissions, Pragmas C / OpenMP / OpenCL
Barrier with atomics Arrays, Barriers, Loop parallelisations, Atomics, Statically-scoped locking, Statically-scoped parallelism, Quantified permissions PVL
Block parallelism Iteration contracts, Loop parallelisations, Statically-scoped parallelism PVL
Invariants and atomics Atomics, Statically-scoped locking PVL
Parallel Block: Blanking Iteration contracts, Arrays, Matrices, Statically-scoped parallelism, Quantified permissions PVL
Permissions: Bad loop (failing case 1) Loop invariants Java
Permissions: Bad loop (failing case 2) Loop invariants Java
Single-threaded counting Loop invariants Java
Single-threaded incrementing Loop invariants Java
Permissions: multi-increment Loop invariants Java
Permissions: Roster (fixed) Lists Java
Permissions: Integer swapping Java
Permissions: Long swapping Java
Permissions: Binary search tree Loop invariants, Stacks, Trees Java
Permissions: Boxing PVL
Predicates: Linked integer list Lists Java
Predicates: Tree traversal Sequences, Trees Java
Predicates: Min-max list Lists Java
Refute: require false Java
Refute: unsatisfiable Java
Refute: bad framing PVL
Refute: refuting (case 1) Java
Refute: refuting (case 2) Java
Refute: refuting (case 3) Java
Refute: refuting (case 4) Java
Refute: refuting (case 5) Java
Synchronisers: CountDownLatch Atomics, Witnesses, Loop invariants Java
Synchronisers: ReentrantLock Atomics, Witnesses, Locking, Loop invariants Java
Synchronisers: Semaphore Atomics, Witnesses, Loop invariants Java
Fork/join incrementing (succeeding) Fork/join concurrency Java
Fork/join incrementing (failing 1) Fork/join concurrency Java
Fork/join incrementing (failing 2) Fork/join concurrency Java
Type casting Trees Java
Using \\\\instanceof and \\\\typeof Java
Longest common prefix Arrays, Loop invariants, Quantified permissions PVL
Relaxed prefix Loop invariants, Quantified permissions PVL
Verifying wait-notify patterns Locking, Fork/join concurrency, Loop invariants PVL
Witnesses: CounterState Witnesses, Loop invariants Java
Witnesses: Getters Witnesses Java
Witnesses: List appending (magic wand) Sequences, Witnesses, Lists, Magic wands Java
Witnesses: List appending (out-of-sync) Sequences, Lists Java
Witnesses: List appending (inline) Sequences, Lists Java
Witnesses: List iterator Witnesses, Lists, Loop invariants, Magic wands Java
Witnesses: Roster Witnesses Java
Recursive trees: Deleting smallest element Sequences, Trees Java
Witnesses: Recursive tree 3 (magic wand) Sequences, Witnesses, Trees, Magic wands Java
Witnesses: Twice Java
Witnesses: Magic wand Witnesses, Loop invariants, Magic wands Java
Witnesses: Magic wand (Silver) Loop invariants, Magic wands Java
Witnesses: Predicates Witnesses Java
GapBuffer Sequences, Arrays, Loop invariants PVL
ColoredTiles Sequences, Iteration contracts, Arrays, Loop invariants, Quantified permissions PVL