AbstractBDDs: A Technique For Using Abstraction in Model Checking

We proof a new methodology for exploiting abstraction in the context of model-checking. Our new technique uses abstract BDDs as its underlying data structure. We show that this technique builds a more refined model than traditional compiler-based methods pr o o ed by Clarke, Grumberg and Long. We also provide experimental results to demonstrate the usefulness ooN method. We have verified a pipelined carry-save multiplier and a simple versioo9 he PCI lo cal bus protocol. Ou