Predicate Abstraction via Symbolic Decision Procedures
| Autor: | Shuvendu K. Lahiri, Thomas Ball, Byron Cook |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2007 |
| Předmět: | |
| Zdroj: | Logical Methods in Computer Science, Vol Volume 3, Issue 2 (2007) |
| Druh dokumentu: | article |
| ISSN: | 1860-5974 85983888 |
| DOI: | 10.2168/LMCS-3(2:1)2007 |
| Popis: | 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. |
| Databáze: | Directory of Open Access Journals |
| Externí odkaz: |
|