| 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 |
|