Solving Bit-vector Equations

O. Möller, H. Rueß

Abstract

This paper is concerned with solving equations on fixed and non-fixed size bit-vector terms. We define an equational transformation system for solving equations on terms where all sizes of bit-vectors and extraction positions are known. This transformation system suggests a generalization for dealing with bit-vectors of unknown size and unknown extraction positions. Both solvers adhere to the principle of splitting bit-vectors only on demand, thereby making them quite effective in practice.

Available as Postscript (223 KB) or compressed Postscript (87 KB).

BibTeX Entry

@InProceedings{MR98:FMCAD,
  title =        "Solving Bit-Vector Equations",
  author =       "Oliver M{\"o}ller and Harald Rue{\ss}",
  booktitle =    "Formal Methods in Computer-Aided Design (FMCAD '98)",
  editor =       "Ganesh Gopalakrishnan and Phillip Windley",
  pages =        "36--48",
  publisher =    "Springer-Verlag",
  series =       "Lecture Notes in Computer Science",
  volume =       "1522",
  month =        nov,
  year =         "1998",
  address =      "Palo Alto, CA",
}

Oliver Möller - March, 12 1999 - Mail to Webmaster