A decision procedure for bit-vector arithmetic

Clark W. Barrett; David L. Dill; Jeremy R. Levitt

doi:10.1145/277044.277186

A decision procedure for bit-vector arithmetic

Clark W. Barrett, David L. Dill, Jeremy R. Levitt

Computer Science

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

Abstract

Bit-vector theories with concatenation and extraction have been shown to be useful and important for hardware verification. We have implemented an extended theory which includes arithmetic. Although deciding equality in such a theory is NP-hard, our implementation is efficient for many practical examples. We believe this to be the first such implementation which is efficient, automatic, and complete.

Original language	English (US)
Title of host publication	Proceedings 1998 - Design and Automation Conference, DAC 1998
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	522-527
Number of pages	6
ISBN (Print)	078034409X
DOIs	https://doi.org/10.1145/277044.277186
State	Published - 1998
Event	35th Design and Automation Conference, DAC 1998 - San Francisco, United States Duration: Jun 15 1998 → Jun 19 1998

Publication series

Name	Proceedings - Design Automation Conference
ISSN (Print)	0738-100X

Conference

Conference	35th Design and Automation Conference, DAC 1998
Country/Territory	United States
City	San Francisco
Period	6/15/98 → 6/19/98

ASJC Scopus subject areas

Computer Science Applications
Control and Systems Engineering
Electrical and Electronic Engineering
Modeling and Simulation
Hardware and Architecture

Access to Document

10.1145/277044.277186

Cite this

A decision procedure for bit-vector arithmetic. / Barrett, Clark W.; Dill, David L.; Levitt, Jeremy R.
Proceedings 1998 - Design and Automation Conference, DAC 1998. Institute of Electrical and Electronics Engineers Inc., 1998. p. 522-527 724527 (Proceedings - Design Automation Conference).

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

Barrett, CW, Dill, DL & Levitt, JR 1998, A decision procedure for bit-vector arithmetic. in Proceedings 1998 - Design and Automation Conference, DAC 1998., 724527, Proceedings - Design Automation Conference, Institute of Electrical and Electronics Engineers Inc., pp. 522-527, 35th Design and Automation Conference, DAC 1998, San Francisco, United States, 6/15/98. https://doi.org/10.1145/277044.277186

@inproceedings{2edd7b295f8048538f22cbc808605de8,

title = "A decision procedure for bit-vector arithmetic",

abstract = "Bit-vector theories with concatenation and extraction have been shown to be useful and important for hardware verification. We have implemented an extended theory which includes arithmetic. Although deciding equality in such a theory is NP-hard, our implementation is efficient for many practical examples. We believe this to be the first such implementation which is efficient, automatic, and complete.",

author = "Barrett, {Clark W.} and Dill, {David L.} and Levitt, {Jeremy R.}",

note = "Publisher Copyright: {\textcopyright} 1998 ACM.; 35th Design and Automation Conference, DAC 1998 ; Conference date: 15-06-1998 Through 19-06-1998",

year = "1998",

doi = "10.1145/277044.277186",

language = "English (US)",

isbn = "078034409X",

series = "Proceedings - Design Automation Conference",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "522--527",

booktitle = "Proceedings 1998 - Design and Automation Conference, DAC 1998",

}

TY - GEN

T1 - A decision procedure for bit-vector arithmetic

AU - Barrett, Clark W.

AU - Dill, David L.

AU - Levitt, Jeremy R.

PY - 1998

Y1 - 1998

N2 - Bit-vector theories with concatenation and extraction have been shown to be useful and important for hardware verification. We have implemented an extended theory which includes arithmetic. Although deciding equality in such a theory is NP-hard, our implementation is efficient for many practical examples. We believe this to be the first such implementation which is efficient, automatic, and complete.

AB - Bit-vector theories with concatenation and extraction have been shown to be useful and important for hardware verification. We have implemented an extended theory which includes arithmetic. Although deciding equality in such a theory is NP-hard, our implementation is efficient for many practical examples. We believe this to be the first such implementation which is efficient, automatic, and complete.

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

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

U2 - 10.1145/277044.277186

DO - 10.1145/277044.277186

M3 - Conference contribution

AN - SCOPUS:0031618668

SN - 078034409X

T3 - Proceedings - Design Automation Conference

SP - 522

EP - 527

BT - Proceedings 1998 - Design and Automation Conference, DAC 1998

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 35th Design and Automation Conference, DAC 1998

Y2 - 15 June 1998 through 19 June 1998

ER -

A decision procedure for bit-vector arithmetic

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this