I hope protocol designers read this paper. The tool in this paper--SMC--uncovered problems in the IEEE Firewire standard in five minutes. The problems were known before, but this paper presents some faster ways to find them. SMC uses finite state automata. It can spot deadlocks and starvation in highly parallel systems. SMC can use either weak or strong fairness. It uses an annotated quotient structure (AQS). The AQS takes advantage of symmetries that appear when there are hundreds of similar components. Another automaton describes the condition that is being tested for. SMC calculates a product graph of this automata and the AQS. It generates nodes in the product graph only as they are needed. Symmetries between product graph nodes give significantly better speed and use less memory.

The paper is a good but complex example of algorithm tuning. The authors compare SMC with Murphi, SYMM, SMV, COSPAN, and other approaches. Researchers in model checking should be interested in this work.