Model Checking, Tla Plus, TLC, Java, Concurrency.
words, if the buffer has capacity 10 and is shared among 5 producers and 5 consumers, the system is deadlock free. This is the configuration our programmer gave up on earlier when his laptop started to smoke. He was right to give up: this system will never deadlock. However, if TLC is started on a