Verifying a Java implementation of a countdown latch. The verification uses witness encoding and handles atomic operations (CAS, axiomatised).
|Features||Atomics, Loop invariants, Witnesses|
|Path to example file||synchronizers/CountDownLatch.java|
|Lines of code||101 lines (comments not included)|
|Lines of specification||60 lines (59.41% of the total)|
|Computation time||19712 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.