Predicate Abstraction via Symbolic Decison Procedures

Shuvendu Lahiri, Thomas Ball, and Byron Cook

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.

Details

Publication typeProceedings
Published inComputer Aided Verification (CAV '05)
Pages15
NumberMSR-TR-2005-53
SeriesLNCS 3576
InstitutionMicrosoft Research
PublisherSpringer Verlag
> Publications > Predicate Abstraction via Symbolic Decison Procedures