ISOMORPH-FREE MODEL ENUMERATION - A NEW METHOD FOR CHECKING RELATIONAL SPECIFICATIONS

Software specifications often involve data structures with huge number s of values, and consequently they cannot be checked using standard st ate exploration or model-checking techniques. Data structures can be e xpressed with binary relations, and operations over such structures ca n be expressed as formulae involving relational variables. Checking pr operties such as preservation of an invariant thus reduces to determin ing the validity of a formula or, equivalently, finding a model (of th e formula's negation). A new method for finding relational models is p resented. It exploits the permutation invariance of models-if two inte rpretations are isomorphic, then neither is a model, or both are-by pa rtitioning the space into equivalence classes of symmetrical interpret ations. Representatives of these classes are constructed incrementally by using the symmetry of the partial interpretation to limit the enum eration of new relation values. The notion of symmetry depends on the type structure of the formula; by picking the weakest typing, larger e quivalence classes (and thus fewer representatives) are obtained. A mo re refined notion of symmetry that exploits the meaning of the relatio nal operators is also described. The method typically leads to exponen tial reductions; in combination with other, simpler, reductions it mak es automatic analysis of relational specifications possible for the fi rst time.