@inproceedings{BRICS-EP-98-MR_SBVE,
  author = 	 "M{\"o}ller, M. Oliver and Rue{\ss}, Harald",
  title = 	 "Solving Bit-Vector Equations",
  booktitle = 	 "Formal Methods in Computer-Aided Design",
  year = 	 1998,
  pages = 	 "36--48",
  month = 	 "",
  crossref = 	 LNCS-1522,
  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."
}

@Proceedings{LNCS-1522,
  editor =       "Ganesh Gopalakrishnan and Phillip Windley",
  booktitle =    "Formal methods in computer aided design: Second
                 International Conference, {FMCAD}'98, Palo Alto, {CA},
                 {USA}, November 4--6, 1998: proceedings",
  title =        "Formal methods in computer aided design: Second
                 International Conference, {FMCAD}'98, Palo Alto, {CA},
                 {USA}, November 4--6, 1998: proceedings",
  volume =       "1522",
  publisher =    "Springer-Verlag Inc.",
  address =      "New York, NY, USA",
  pages =        "ix + 529 (or ix + 528??)",
  year =         "1999",
  ISBN =         "3-540-65191-8",
  LCCN =         "TK7874.65 .F53 1998",
  bibdate =      "Sat Jan 9 14:35:31 MST 1999",
  series =       "Lecture Notes in Computer Science",
  acknowledgement = ack-nhfb,
}