Predicate Abstraction via Symbolic Decision Procedures
<|reference_start|>Predicate Abstraction via Symbolic Decision Procedures: 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.<|reference_end|>
@article{lahiri2006predicate,
    title={Predicate Abstraction via Symbolic Decision Procedures},
    author={Shuvendu K. Lahiri, Thomas Ball, Byron Cook},
    journal={Logical Methods in Computer Science, Volume 3, Issue 2 (April 24,
  2007) lmcs:2218},
    year={2006},
    doi={10.2168/LMCS-3(2:1)2007},
    archivePrefix={arXiv},
    eprint={cs/0612003},
    primaryClass={cs.LO cs.PL cs.SC}
}