Name
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 datatypes. 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 | DOI | Venue |
|---|---|---|
2009 | 10.1007/s10009-009-0101-x | STTT |
Keywords | Field | DocType |
original bit-vector formula,boolean variable,previous under-approximation,bit-vector · decision-procedures,new decision procedure,decision procedure,arbitrary bit-vector operation,bit-vector variable,abstraction-based decision procedure,fewer boolean variable,competing decision procedure,finite-precision bit-vector arithmetic,propositional logic,satisfiability,sat solver | Constraint satisfaction,Model checking,Computer science,Unsatisfiable core,Boolean satisfiability problem,Propositional calculus,Arithmetic,Theoretical computer science,Data type,Boolean algebra,Boolean data type | Journal |
Volume | Issue | ISSN |
11 | 2 | 1433-2787 |
Citations | PageRank | References |
12 | 0.70 | 16 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Randal E. Bryant | 1 | 9204 | 1194.64 |
| Daniel Kroening | 2 | 3084 | 187.60 |
| Joël Ouaknine | 3 | 1481 | 99.25 |
| Sanjit A. Seshia | 4 | 2226 | 168.09 |
| Ofer Strichman | 5 | 1071 | 63.61 |
| Bryan Brady | 6 | 72 | 4.17 |