    

An Efficient Decision Procedure for the Theorz of FixedSized BitVectors
by Dr. Harald Rueß, David Cryluk & Oliver Möller.
Abstract
In this paper we describe a decision procedure for the core theory of fixedsized bitvectors with extraction and composition than can readily be integrated into Shostak's procedure for deciding combinations of theories. Inputs to the solver are unquantified bitvector equations
t = u and the algorithm returns true if t = u is valid in the bitvector 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 + n^{2}), where t is the length of the bitvector term t and n denotes the number of bits on either side of the equation. Then, the solver for the core bitvector theory is extended to handle other bitvector operations like bitwise logical operations, shifting, and arithmetic interpretations of bitvectors. We develop a BDDlike datastructure called bitvector BDDs to represent bitvectors, various operations on bitvectors, and a solver on bitvector 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 bitvectors we have simplified a number of proofs by eliminating manual proof steps that were previously necessary for reasoning about bitvectors.
Files


