TopSpin
swMATH ID: | 972 |
Software Authors: | Donaldson, Alastair; Miller, Alice |
Description: | 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. |
Homepage: | http://www.doc.ic.ac.uk/~afd/topspin/ |
Dependencies: | SPIN |
Related Software: | SPIN; SymmSpin; GAP; Uppaal; nauty; Spin-to-Grape; PROMELA; CUDD; TransGrp; Traces; jSpin; Z2sal; Atelier B; B4Free; ProB; Rodin; SLAM; DDVerify; SatAbs; Bebop |
Cited in: | 11 Documents |
all
top 5
Cited by 20 Authors
all
top 5
Cited in 7 Serials
Cited in 3 Fields
10 | Computer science (68-XX) |
3 | Group theory and generalizations (20-XX) |
1 | Mathematical logic and foundations (03-XX) |