  We present a new approach for performing predicate abstraction based on
symbolic decision procedures. Intuitively, a symbolic decision procedure for a
theory takes a set of predicates in the theory and symbolically executes a
decision procedure on all the subsets over the set of predicates. The result of
the symbolic decision procedure is a shared expression (represented by a
directed acyclic graph) that implicitly represents the answer to a predicate
abstraction query.
  We present symbolic decision procedures for the logic of Equality and
Uninterpreted Functions (EUF) and Difference logic (DIFF) and show that these
procedures run in pseudo-polynomial (rather than exponential) time. We then
provide a method to construct symbolic decision procedures for simple mixed
theories (including the two theories mentioned above) using an extension of the
Nelson-Oppen combination method. We present preliminary evaluation of our
Procedure on predicate abstraction benchmarks from device driver verification
in SLAM.
