Lahiri, Shuvendu K. and Ball, Thomas and Cook, Byron - Predicate Abstraction via Symbolic Decision Procedures

lmcs:2218 - Logical Methods in Computer Science, April 24, 2007, Volume 3, Issue 2
Predicate Abstraction via Symbolic Decision Procedures

Authors: Lahiri, Shuvendu K. and Ball, Thomas and Cook, Byron

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.


Source : oai:arXiv.org:cs/0612003
DOI : 10.2168/LMCS-3(2:1)2007
Volume: Volume 3, Issue 2
Published on: April 24, 2007
Submitted on: May 31, 2006
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Computer Science - Symbolic Computation,F.3.1,F.4.1


Share

Consultation statistics

This page has been seen 40 times.
This article's PDF has been downloaded 27 times.