In this example case a re-entrant lock, implemented in Java, is verified. An atomic integer is used as the synchroniser.
|Features||Atomics, Locking, Loop invariants, Witnesses|
|Path to example file||synchronizers/ReentrantLock.java|
|Lines of code||140 lines (comments not included)|
|Lines of specification||81 lines (57.86% of the total)|
|Computation time||20853 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.