Paper Info
Title
Deciding bit-vector arithmetic with abstraction
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 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.
Year
Venue
Keywords
2007
TACAS
original bit-vector formula,boolean variable,previous under-approximation,original formula,new decision procedure,arbitrary bit-vector operation,bit-vector variable,fewer boolean variable,competing decision procedure,procedure alternate,bit-vector arithmetic,satisfiability,propositional logic,sat solver
Field
DocType
Volume
Discrete mathematics,Computer science,Boolean satisfiability problem,Satisfiability,Unsatisfiable core,Arithmetic,Propositional calculus,Theoretical computer science,Conjunctive normal form,Resolution (logic),Boolean data type,Bit array
Conference
4424
ISSN
Citations 
PageRank 
0302-9743
56
3.09
References 
Authors
16
6
Name
Order
Citations
PageRank
Randal E. Bryant192041194.64
Daniel Kroening23084187.60
Joël Ouaknine3148199.25
Sanjit A. Seshia42226168.09
Ofer Strichman5107163.61
Bryan Brady6724.17