Automatic Symmetry Reduction for the SPIN Model Checker. TopSPIN is an automatic symmetry reduction tool for the SPIN model checker. TopSPIN is applied to a Promela specification, and, provided that the specification adheres to some restrictions (detailed in the user manual), uses computational group theory to automatically determine a group of component symmetries associated with the specification. The tool automatically modifies the model checking algorithm employed by SPIN to exploit these symmetries during verification. This can result in significantly reduced memory consumption, and in many cases also in faster verification time.