We propose 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 proposed by Clarke, Grumberg and Long. We also provide experimental results to demonstrate the usefulness of our method. We have verified a pipelined carry-save multiplier and a simple version of the PCI local bus protocol. Our verification of the PCI bus revealed a subtle inconsistency in the PCI standard. We believe this is an interesting result by itself.
CITATION STYLE
Clarke, E., Jha, S., Lu, Y., & Wang, D. (1999). Abstract BDDs: A technique for using abstraction in model checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1703, pp. 172–187). Springer Verlag. https://doi.org/10.1007/3-540-48153-2_14
Mendeley helps you to discover research relevant for your work.