Deciding Bit-Vector Arithmetic with Abstraction

ion Randal E. Bryant1 , Daniel Kroening2 , Jo¨el Ouaknine3 , Sanjit A. Seshia4 , Ofer Strichman5 , and Bryan Brady4 1 Carnegie Mellon University, Pittsburgh 2 ETH Z¨urich 3 Oxford University Computing Laboratory 4 University of California, Berkeley 5 The Technion, Haifa Abstract. We present a new decision procedure for finite-precision bitvector 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 underapproximation 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 underapproximati...

• Type: Conference
• Year: 2007
• Where: TACAS
• Authors: Randal E. Bryant, Daniel Kroening, Joël Ouaknine, Sanjit A. Seshia, Ofer Strichman, Bryan A. Brady
• Keywords: Algorithms, Bit-vector Variables, Boolean Variables, Decision Procedures, TACAS 2007