Abstraction and BDDs complement SAT-based BMC in DiVer

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

doi:10.1007/978-3-540-45069-6_20

Abstraction and BDDs complement SAT-based BMC in DiVer

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

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Chapter

19 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 language	English (US)
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Editors	Warren A. Hunt, Fabio Somenzi
Publisher	Springer Verlag
Pages	206-209
Number of pages	4
ISBN (Print)	3540405240, 9783540405245
DOIs	https://doi.org/10.1007/978-3-540-45069-6_20
State	Published - 2003

Publication series

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

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-540-45069-6_20

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

Gupta, Aarti ; Ganai, Malay ; Wang, Chao et al. / Abstraction and BDDs complement SAT-based BMC in DiVer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Warren A. Hunt ; Fabio Somenzi. Springer Verlag, 2003. pp. 206-209 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{a15e7cbcf3aa413ebadf92baacc3219b,

title = "Abstraction and BDDs complement SAT-based BMC in DiVer",

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.",

author = "Aarti Gupta and Malay Ganai and Chao Wang and Zijiang Yang and Pranav Ashar",

year = "2003",

doi = "10.1007/978-3-540-45069-6_20",

language = "English (US)",

isbn = "3540405240",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "206--209",

editor = "Hunt, {Warren A.} and Fabio Somenzi",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

address = "Germany",

}

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

Abstraction and BDDs complement SAT-based BMC in DiVer. / Gupta, Aarti; Ganai, Malay; Wang, Chao et al.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Warren A. Hunt; Fabio Somenzi. Springer Verlag, 2003. p. 206-209 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2725).

Research output: Chapter in Book/Report/Conference proceeding › Chapter

TY - CHAP

T1 - Abstraction and BDDs complement SAT-based BMC in DiVer

AU - Gupta, Aarti

AU - Ganai, Malay

AU - Wang, Chao

AU - Yang, Zijiang

AU - Ashar, Pranav

PY - 2003

Y1 - 2003

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=35248874847&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35248874847&partnerID=8YFLogxK

U2 - 10.1007/978-3-540-45069-6_20

DO - 10.1007/978-3-540-45069-6_20

M3 - Chapter

AN - SCOPUS:35248874847

SN - 3540405240

SN - 9783540405245

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 206

EP - 209

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Hunt, Warren A.

A2 - Somenzi, Fabio

PB - Springer Verlag

ER -

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

Abstraction and BDDs complement SAT-based BMC in DiVer

Abstract

Publication series

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this