Verifying a wait/notify concurrency pattern, in the context of two workers/threads that concurrently operate on a shared Queue. When working on the queue all other threads have to _wait_ for completion, and when the working threads has finished it _notifies_ all other waiting threads.
Fork/join concurrency, Locking, Loop invariants
Path to example file
Lines of code
25 lines (comments not included)
Lines of specification
4 lines (16% of the total)
Note, verification may take a while and has a time-out of 20 seconds.