## An abstraction-based decision procedure for bit-vector arithmetic

*Randal E. Bryant*, *Daniel Kroening*, *Joël
Ouaknine*, *Sanjit A. Seshia*, *Ofer Strichman*,
and *Bryan Brady*
We present a new decision procedure for finite-precision bit-vector
arithmetic with arbitrary bit-vector operations. Such decision
procedures are essential components of verifications systems, whether
the domain of interest is hardware, such as in word-level bounded
model-checking of circuits, or software, where one must often reason
about programs with finite-precision datatypes. Our procedure
alternates between generating under- and over-approximations of the
original bit-vector formula. An under-approximation is obtained by a
translation to propositional logic in which some bit-vector variables
are encoded with fewer Boolean variables than their width. If the
under-approximation is unsatisfiable, we use the unsatisfiable core to
derive an over-approximation based on the subset of predicates that
participated in the proof of unsatisfiability. If this
over-approximation is satisfiable, the satisfying assignment guides
the refinement of the previous under-approximation by increasing, for
some bit-vector variables, the number of Boolean variables that encode
them. We present experimental results that suggest that this
abstraction-based approach can be considerably more efficient than
directly invoking the SAT solver on the original formula as well as
other competing decision procedures.

*International Journal on
Software Tools for Technology Transfer* 11(2), 2009. 10 pages.

PDF
© 2009 Springer-Verlag.

Imprint / Data Protection