Single producer and single-consumer verification using AtomicInteger. The contracts for the AtomicInteger is the version without magic-wand (delta).
|Path to example file||atomics/RBProdCons.java|
|Lines of code||141 lines (comments not included)|
|Lines of specification||59 lines (41.84% of the total)|
|Computation time||19242 milliseconds|
Note, verification may take a while and has a time-out of 20 seconds.