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.

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