Predicate Abstraction via Symbolic Decison Procedures

We present a new approach for performing predicate abstraction based on symbolic decision procedures. A symbolic decision procedure for a theory T (\SDP_T) takes sets of predicates G and E and symbolically executes a decision procedure for T on G' ˘ neg e ;|; e \in E$, for all the subsets G' of G. The result of \SDP_T 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.

tr-2005-53.pdf
PDF file

In  Computer Aided Verification (CAV '05)

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details

TypeProceedings
Pages15
NumberMSR-TR-2005-53
SeriesLNCS 3576
InstitutionMicrosoft Research
> Publications > Predicate Abstraction via Symbolic Decison Procedures