Invariants and atomics
This is a example verification case with atomic blocks and resource invariants, in the style of CSL. This file contains several methods, some of which verify and some not.
|Features||Atomics, Statically-scoped locking|
|Path to example file||parallel/inv-test.pvl|
|Lines of code||55 lines (comments not included)|
|Lines of specification||9 lines (16.36% of the total)|
|Computation time||23064 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.