SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

An Efficient Decision Procedure for the Theorz of Fixed-Sized Bit-Vectors
 by Dr. Harald Rueß, David Cryluk & Oliver Möller.

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 | . Zag n + n2), 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.


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2019 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy