@inproceedings{lahiri2007predicate,
author = {Lahiri, Shuvendu and Ball, Thomas and Cook, Byron},
title = {Predicate Abstraction via Symbolic Decision Procedures},
booktitle = {Logical Methods in Computer Science (LMCS '07)},
year = {2007},
month = {January},
abstract = {We present a new approach for performing predicate abstraction based on symbolic decision procedures. Intuitively, a symbolic decision procedure for a theory takes a set of predicates in the theory and symbolically executes a decision procedure on all the subsets over the set of predicates. The result of the symbolic decision procedure 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 (DIFF) and show that these procedures run in pseudo-polynomial (rather than exponential) time. We then provide a method to construct symbolic decision procedures for simple mixed theories (including the two theories mentioned above) 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.},
url = {http://approjects.co.za/?big=en-us/research/publication/predicate-abstraction-via-symbolic-decision-procedures/},
volume = {3},
edition = {Logical Methods in Computer Science (LMCS '07)},
}