Model Checking, Tla Plus, TLC, Java, Concurrency.
not our unfortunate programmer’s laptop). The analysis of the trace reveals the flaw in the buffer implementation: all the threads (producers and consumers) are waiting in the same wait set. When method get calls notify, the intent is to notify a producer that a slot has been made available in the