Computing Predicate Abstractions by Integrating BDDs and SMT Solvers

The efficient computation of exact abstractions of a concrete program for a given set of predicates is key to the efficiency of Counter-Example Guided Abstraction-Refinement (CEGAR). Recent work propose the use of DPLL-based SMT solvers, modified into enumerators. This technique has been successfully applied in the realm of software, where a control flow graph is available to direct the exploration. However this approach shows some limitations when the number of models grows: in fact, it intrinsically relies on the enumeration of all the implicants, which basically requires the enumerations of all the disjuncts in the DNF of the abstraction. In this paper, we propose a new technique to improve the construction of abstractions. We complement SMT solvers with the use of BDDs, which enables us to avoid the model explosion. Essentially, we exploit the fact that BDDs are a DAG representations of the space that a DPLL-based enumerator treats as a tree. A preliminary experimental evaluation shows the potential of the approach.