Solving Bitvector Equations

Presented at FMCAD'98, Palo Alto, CA, November 1997; © Springer-Verlag.

---

Authors

M. Oliver Möller and Harald 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.

gzipped postscript or postscript

BibTeX Entry

@inproceedings{MoellerRuess:FMCAD98,
  author =       "M{\"o}ller, M. Oliver and Rue{\ss}, Harald",
  title =        "Solving Bit-Vector Equations",
  booktitle =    "Formal methods in computer aided design: Second
                 International Conference, {FMCAD}'98",
  editor =       "Ganesh Gopalakrishnan and Phillip Windley",	 
  year =         1998,
  pages =        "36--48",
  series =       LNCS,
  number =       1522,
  publisher =    "Springer-Verlag"
}

---

Harald Ruess: ruess@csl.sri.com