@article { 130, title = {Deciding Bit-Vector Arithmetic with Abstraction}, journal = {Software Tools for Technology Transfer (STTT)}, volume = {11}, year = {2009}, pages = {95--104}, publisher = {Springer}, abstract = {

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 data-types. 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.

}, URL = {http://www.kroening.com/publications/view-publications-bkossb2008-sttt.html}, author = {Bryant, R and Kroening, D and Ouaknine, J and Seshia, S and Strichman, O and Brady, B} }