Predicate abstraction via symbolic decision procedures

Abstract

We present a new approach for performing predicate abstraction based on symbolic decision procedures. A symbolic decision procedure for a theory T (SDPT) takes sets of predicates G and E and symbolically executes a decision procedure for T on G′ ∪ {¬ e | e ∈ E}, for all the subsets G′ of G. The result of SDPT 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 (DIF) and show that these procedures run in pseudo-polynomial (rather than exponential) time. We then provide a method to construct SDP's for simple mixed theories (including EUF + DIF) 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. © Springer-Verlag Berlin Heidelberg 2005.