Tecnical Report CMU-CS-94-219.
Sorry, no postscript available.
This paper argues that, while proving properties of designs may be intractable, detecting errors may not be. State transitions of an operation can be enumerated exhaustively, within a 'scope' defined by the user that places a bound on the size of state components. Symmetry can then be exploited to reduce this finite state space. A state can be shown to be symmetrical, in the context of the analysis, to a state already examined, and thus guaranteed not to reveal an error.
Preliminary experiments with a prototype are promising. A small scope often seems sufficient to catch errors, and exhibits enough symmetry to reduce search by a factor of 10 or more.