@techreport{lahiri2005predicate,
author = {Lahiri, Shuvendu and Ball, Thomas and Cook, Byron},
title = {Predicate Abstraction via Symbolic Decison Procedures},
series = {LNCS 3576},
year = {2005},
month = {April},
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' ˘ 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.},
publisher = {Springer Verlag},
url = {http://approjects.co.za/?big=en-us/research/publication/predicate-abstraction-via-symbolic-decison-procedures/},
pages = {15},
edition = {Computer Aided Verification (CAV '05)},
number = {MSR-TR-2005-53},
note = {Computer Aided Verification (CAV '05)},
}