Model-based reasoning: locking protocol
Verification example where model-based reasoning is used to verify that the program adheres to a certain locking protocol.
|Path to example file||futures/locking.pvl|
|Lines of code||80 lines (comments not included)|
|Lines of specification||36 lines (45% of the total)|
|Computation time||25560 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.