Boolean compilation of relational specifications

Relational specifications, in which the states themselves are characterized by relations, have wide application in software design but, until now, limited support from automated tools. This paper describes a new method for finding errors in a relational specification. A property to be checked is cast as a relational formula, which, if the property holds, has no finite models. The user selects a ‘scope ’ that bounds the size of candidate models. The relational formula is then translated into a boolean formula that has a model for every model of the relational formula within that scope. The boolean formula is represented in conjunctive normal form (CNF), being both a good match for relational formulae and the required input format of the most efficient boolean solvers. Certain features of the boolean formula, however, cause an exponential blowup if a direct translation is attempted. But by using some simple strategies – case splitting, variable introduction, symmetry breaking and negation caching – it is possible to overcome these problems and make translation efficient. The resulting boolean formulae, although often huge, are easily handled by WalkSAT, a stochastic solver. For a variety of specifications we examined, compilation and solving together take less than 10 seconds.