A uniform framework for predicate abstraction approximation

Abstract. Abstraction refinement is a powerful technique that enables the verification of real systems. An initial coarse abstraction is provided and iteratively refined until either the property is proved to be true or false. Computing a precise abstraction is usually very expensive. Thus, many techniques have been conceived in order to approximate the ab-stract transition relation. In the framework of predicate abstraction, ex-amples of such techniques are early quantification, Cartesian approx-imation, maximum cube length approximation, predicate partitioning, and interpolation-based approximation. When such approximations are employed, adding new predicates is no more sufficient to rule out all spu-rious counterexamples. Standard model checkers add new contraints to the transition relations in order to refine the approximation. We propose a uniform framework for describing most of known approx-imation techniques. The mapping among various techniques provides a conceptual basis for the development of new algorithms.