**Published in CAV'97, pages 60-71 **

**Abstract**

In this paper we describe a decision procedure for the core theory of
fixed-sized bit-vectors with extraction and composition than can readily
be integrated into Shostak's procedure for deciding combinations of theories.
Inputs to the solver are unquantified bit-vector equations *t = u*
and the algorithm returns *true* if *t = u* is valid in the bit-vector
theory, *false* if *t = u* is unsatisfiable, and a system of
solved equations otherwise. The time complexity of the solver is *O(|t|*log(n)
+ n^2)*, where *t* is the length of the bit-vector term *t*
and *n* denotes the number of bits on either side of the equation.
Then, the solver for the core bit-vector theory is extended to handle other
bit-vector operations like bitwise logical operations, shifting, and arithmetic
interpretations of bit-vectors. We develop a BDD-like data-structure called
bit-vector BDDs to represent bit-vectors, various operations on bit-vectors,
and a solver on bit-vector BDDs. The overall procedure has been integrated
with the decision procedures of the PVS prover. The implementation has
been tested with typical lemmas from the domain of microprocessor verification.
The implementation has also been applied to proofs found in the verification
of a commercial microprocessor. By using our decision procedure for bit-vectors
we have simplified a number of proofs by eliminating manual proof steps
that were previously necessary for reasoning about bit-vectors.

Available as Postscript (227 KB) or compressed Postscript (89 KB).

**BibTeX Entry**

@INPROCEEDINGS{cav97*60, AUTHOR = {Cyrluk, David and M{\"o}ller, Oliver and Rue{\ss}, Harald}, TITLE = {An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors}, BOOKTITLE = {Computer Aided Verification. 9th International Conference (CAV97). Haifa, Israel, June 22-25, 1997: Proceedings}, PAGES = {60-71}, CROSSREF = {cav97},} @PROCEEDINGS{cav97, TITLE = {Computer Aided Verification. 9th International Conference (CAV97). Haifa, Israel, June 22-25, 1997: Proceedings}, EDITOR = {Grumberg, Orna}, PUBLISHER = {Springer}, ADDRESS = {Berlin - Heidelberg - New York}, YEAR = {1997}, SERIES = {Lecture Notes in Computer Science LNCS}, VOLUME = {1254}, LOCATION = {DFKI Saarbr{\"u}cken}, DFKINUMBER = {M:S97-233}, SIGNATURE = {A-0020-117:2}, ISBN = {3-540-63166-6}, STATUS = {available}, CRINDEX = {A.0 General Literature - Conference Proceedings}, BIBTYPE = {PROCEEDINGS},}

Oliver Möller - March 26, 1998 - Mail to Webmaster