Abstraction and BDDs complement SAT-based BMC in DiVer

Aarti Gupta, Malay Ganai, Chao Wang, Zijiang Yang, Pranav Ashar

Research output: Chapter in Book/Report/Conference proceedingChapter

18 Scopus citations

Abstract

Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity for finding bugs in large designs. However, due to its incompleteness, there is a need to perform deeper searches for counterexamples, or a proof by induction where possible. The DiVer verification platform uses abstraction and BDDs to complement BMC in the quest for completeness. We demonstrate the effectiveness of our approach in practice on industrial designs.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsWarren A. Hunt, Fabio Somenzi
PublisherSpringer Verlag
Pages206-209
Number of pages4
ISBN (Print)3540405240, 9783540405245
DOIs
StatePublished - 2003
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2725
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Abstraction and BDDs complement SAT-based BMC in DiVer'. Together they form a unique fingerprint.

  • Cite this

    Gupta, A., Ganai, M., Wang, C., Yang, Z., & Ashar, P. (2003). Abstraction and BDDs complement SAT-based BMC in DiVer. In W. A. Hunt, & F. Somenzi (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 206-209). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2725). Springer Verlag. https://doi.org/10.1007/978-3-540-45069-6_20