A decision procedure for bit-vector arithmetic

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 languageEnglish (US)
Title of host publicationProceedings 1998 - Design and Automation Conference, DAC 1998
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages6
ISBN (Print)078034409X
StatePublished - 1998
Event35th Design and Automation Conference, DAC 1998 - San Francisco, United States
Duration: Jun 15 1998Jun 19 1998

Publication series

NameProceedings - Design Automation Conference
ISSN (Print)0738-100X


Conference35th Design and Automation Conference, DAC 1998
Country/TerritoryUnited States
CitySan Francisco

ASJC Scopus subject areas

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


Dive into the research topics of 'A decision procedure for bit-vector arithmetic'. Together they form a unique fingerprint.

Cite this