# Faster Checking of Software Specifications By Eliminating Isomorphs

**Authors:**Daniel Jackson, Somesh Jha, and Craig A. Damon
* Proc. ACM Conf. on Principles of Programming Languages *,
January 1996.

Download the PostScript.

## Abstract

Both software specifications and their intended properties can be
expressed in a simple relational calculus. The claim that a specification
satisfies a property becomes a relational formula that can be checked
automatically by enumerating the formula's interpretations. Because the
number of interpretations is usually huge, this approach has not been
thought to be practical. But by eliminating isomorphic interpretations, the
enumeration can be reduced substantially, by a factor of k! for each basic
type of k elements.
### Keywords:

model checking, symmetry, relational calculus, formal specification, Z.

Back to Nitpick Home Page