OpenMP: Parallel sections (succeeding)
Demonstrates how two loops that must be fused to be race free can be specified and verified.
|Language||OpenMP for C|
|Features||Arrays, Iteration contracts, Loop parallelisations, Pragmas, Quantified permissions|
|Path to example file||openmp/sections-reduced.c|
|Lines of code||106 lines (comments not included)|
|Lines of specification||22 lines (20.75% of the total)|
|Computation time||42225 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.