Classical Owicki-Gries verification example: forking two threads that write to a shared location.
|Features||Fork/join concurrency, Locking|
|Path to example file||manual/OwickiGries.pvl|
|Lines of code||16 lines (comments not included)|
|Lines of specification||1 lines (6.25% of the total)|
|Computation time||21137 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.