Predicate Abstraction: Predicate abstraction (Graf and Saïdi 1997), is a special case of an over-approximating data abstraction which maps a potentially infinite-state program into a finite-state program, via a finite set of predicates over the program’s variables. Predicate abstraction allows you to build an abstract program in a fully automatic way, and it forms the basis of numerous automated abstract model-checking tools (Ball et al. 2001; Henzinger et al. 2002; Chaki et al. 2004). The basic idea is to replace a concrete program variable by a Boolean variable that evaluates to a given Boolean formula (a predicate) over the original variable. This concept can be easily extended to handle multiple predicates and, more interestingly, predicates over multiple variables. For example, assume we have a program with two integer variables, x and y, which can grow infinitely. This program will have an infinite state space and model checking cannot be complete in general. However, if the only relationship of interest between the two variables is their equality, we can use a predicate representing this relationship, B ≡ x==y, to construct an abstract program as follows. (We used similar abstraction when analyzing DEOS):
1. Wherever the condition x==y appears in the program, we replace it with the condition B==true, and
2. Whenever there is an operation involving x or y, we replace it with an operation changing the value of B appropriately.