Model Checking, Tla Plus, TLC, Java, Concurrency.
are not easily reproducible. Such bugs can be real nightmares. There is something wrong with your system, you know it, you have seen it, but until you can make it happen again, you don’t know how to approach the problem. To illustrate this difficulty, consider the classic example of a shared buffer