Predicate abstraction is a method used for checking software systems. One looks for a model with a reduced state space; the original data variables are eliminated, and each predicate is represented by a Boolean variable that represents its truth value. One collects all of these values in a Boolean vector.

The abstract transition relation B associated with a program P links the vector to the vector if there are states u and v such that:

i. The vector of values of predicates in the state u is ,

ii. The vector of values in the state v is , and

iii. When P operates on u, the final state is v.

Then, B can be seen as the model of P, and the goal of the paper is to describe B, namely, the set of , such that and are linked.

After a good introduction to predicate abstraction, the major contribution of the paper is in paragraphs 2 and 3: one can get B as a conjunctive normal form (CNF) formula from the program by preprocessing, and one can enumerate B with a fast satisfiability (SAT) solver. The implementation is mentioned in paragraph 4, and experimental results in paragraph 5.

This paper is something of an announcement, rather than a final description of a process that is clearly very involved. For instance, the authors offer plausible arguments for the efficiency of their method, but without any proof.