##
This **preview** shows page *1-2-3-4-5*
out of 15 **pages**.

*View Full Document*

End of preview. Want to read all 15 pages?

Upload your study docs or become a GradeBuddy member to access this document.

View Full Document**Unformatted text preview:**

Deciding Bit-Vector Arithmetic withAbstraction?Randal E. Bryant1, Daniel Kroening2, Jo¨el Ouaknine3, Sanjit A. Seshia4,Ofer Strichman5, and Bryan Brady41Carnegie Mellon University, Pittsburgh2ETH Z¨urich3Oxford University Computing Laboratory4University of California, Berkeley5The Technion, HaifaAbstract. We present a new decision procedure for finite-precision bit-vector arithmetic with arbitrary bit-vector operations. Our procedurealternates b etween generating under- and over-approximations of theoriginal bit-vector formula. An under-approximation is obtained by atranslation to propositional logic in which some bit-vector variables areenco de d with fewer Boolean variables than their width. If the under-approximation is unsatisfiable, we use the unsatisfiable core to derive anover-approximation based on the subset of predicates that participatedin 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 numb erof Boolean variables that encode them. We present experimental resultsthat suggest that this abstraction-based approach can be considerablymore efficient than directly invoking the SAT solver on the original for-mula as well as other competing decision procedures.1 IntroductionDecision procedures for quantifier-free fragments of first-order logic find wide-spread use in hardware and software verification. Current uses of decision pro-cedures fall into one of two extremes. At one end, a Boolean satisfiability solveris directly employed as the decision procedure, with systems modeled at thebit-level. Sample applications of this kind include bounded model checking [1,2] and SAT-based program analysis [3]. At the other extreme, verifiers use deci-sion procedures that reason over arbitrary-precision abstract types such as theintegers and reals (Z and R).In reality, system descriptions are best modeled with a level of precision thatis somewhere in between. System descriptions are usually at the word-level; i.e.,?B. Brady, R. E. Bryant, and S. A. Seshia were supported in part by SRC contract1355.001. This research was also supported in part by the MARCO Gigascale Sys-tems Res earch Center and by NSF grant CNS-0627734.they use finite-precision arithmetic and bit-wise op erations on bit-vectors. Thedirect use of a SAT solver as cited earlier (also known as “bit-blasting”) is theconceptually simplest way to implement a bit-vector decision pro ce dure eventhough it ignores higher-level structure present in the original decision problem.However, the bit-blasting approach can be too computationally expensive inpractice (see, for example, [4]). There is therefore a pressing need for betterdecision procedures for bit-vector arithmetic.Contribution We present a decision proce dure for quantifier-free bit-vector arith-metic that uses automatic abstraction-refinement. This procedure is now im-plemented in the verification system uclid, and we shall call it by this namefrom hereon. Given an input bit-vector formula φ, uclid first builds an under-approximation φ from φ by restricting the number of Boolean variables usedto encode each bit-vector variable (see details of this encoding in Section 3.1).The reduced formula is typically much smaller and easier to solve. If φ is sat-isfiable, so is φ, and the algorithm terminates. In case the Boolean formula isfound to be unsatisfiable, the SAT solver is able to output a resolution proof ofthis fact, from which the unsatisfiable core use d in this proof can be extracted.Using this core, an over-approximation φ is built. This over-approximation usesthe full set of bits of the original vectors, but only a subset of the constraints.This subset is determined by examining the unsatisfiable core of φ. If φ is un-satisfiable, so is φ, and uclid terminates. Otherwise, the algorithm refines theunder-approximation φ by increasing, for at least one bit-vector variable, thenumbe r of Boolean variables encoding it. Specifically, the new size is implied bythe value of this variable in the s atisfying assignment to φ. This process is re-peated until the original formula is shown to be either satisfiable or unsatisfiable.The algorithm is trivially guaranteed to terminate due to the finite domain.This approach has the potential of being efficient in one of the following twoscenarios:1. The bit-vector formula is satisfiable, and a solution can be represented witha small number of bits.2. The bit-vector formula is unsatisfiable, and a relatively small number ofterms in this formula participate in the proof (i.e., the proof still holds afterreplacing the other terms with inputs).Whether this potential is fulfilled depends on one’s ability to find such smallsolutions and small unsatisfiable cores6efficiently: For the former, we search forgradually increasing solutions in terms of the number of bits that are neededin order to represent them, and hence are guaranteed to find a small one if itexists; For the latter, modern SAT solvers are quite apt at finding small cores6A small unsatisfiable core of the CNF encoding of a formula does not necessarilyimply that a small number of terms from the original formula are necessary for theproof, but obviously the two measures are correlated.when they exist. In practice, as our experiments show, one of these conditionsfrequently holds and we are able to detect it with our tool faster than analyzingthe formula head-on without any approximations.Our approach can be seen as an adaptation to bit-vector formulas of our previ-ous work [5] on abstraction-refinement of quantifier-free Presburger Arithmetic,which, in turn, was inspired by the proof-based abstraction-refinement approachto model checking proposed by McMillan and Amla [6]. Other than the differ-ent problem domain (bit-vectors vs. Presburger formulas), we also extend thetheoretical framework to operate on an arbitrary circuit representation of theformula, rather than on a CNF representation. We also employ optimizationsspecific to bit-vector arithmetic. On the applied side, we report experimentalresults on a set of benchmarks generated in both hardware and software veri-fication. Our experiments suggest that our approach can be considerably moreefficient than directly invoking the SAT solver on the original formula as well asother state-of-the-art decision procedures.Related Work Current decision procedures