Abstract. We give a detailed description of SymmSpin, a symmetryreduction package for Spin. It o ers four strategies for state-space reduction, based on the heuristic that we presented in 3 , and a fth mode for reference. A series of new experiments is described, underlining the e ectiveness of the heuristic and demonstrating the generalisation of the implementation to multiple scalar sets, multiple process families, as well as almost the full Promela language.