We present a new approach for performing predicate abstraction based on symbolic decision procedures. A symbolic decision procedure for a theory T (\SDP_T) takes sets of predicates G and E and symbolically executes a decision procedure for T on G' ˘ neg e ;|; e \in E$, for all the subsets G' of G. The result of \SDP_T 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.

PDF file

In: Computer Aided Verification (CAV '05)

Publisher: Springer Verlag
All copyrights reserved by Springer 2007.

Details