Shuvendu Lahiri, Thomas Ball, and Byron Cook
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.
In Computer Aided Verification (CAV '05)
Publisher Springer Verlag
All copyrights reserved by Springer 2007.