## Deciding bit-vector arithmetic with abstraction

*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. 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.

*Proceedings of TACAS 07*, LNCS 4424, 2007. 15 pages.

PDF
© 2007
Springer-Verlag.

Imprint / Data Protection