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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jun 01, 1998
Accession Number
ADA400400

Entities

People

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

Organizations

  • Stanford University

Tags

Communities of Interest

  • C4I
  • Human Systems

DTIC Thesaurus Topics

  • Algorithms
  • Arithmetic
  • Automatic
  • Automation
  • Coefficients
  • Complex Variables
  • Computers
  • Engineering
  • Equations
  • Extraction
  • Microprocessors
  • National Security
  • Notation
  • Reasoning
  • Universities
  • Verification

Fields of Study

  • Mathematics

Readers

  • Computer Programming and Software Development.
  • Operations Research