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 (SDPT) takes sets of predicates G and E and symbolically executes a decision procedure for T on G' ˘ neg 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.
|Published in||Computer Aided Verification (CAV '05)|
All copyrights reserved by Springer 2007.