Abstract: Rarely verification problems originate from bit-level descriptions. Yet, most of the verification technologies are based on bit-blasting, i.e., reduction to Boolean reasoning. In this thesis we advocate reasoning at higher level of abstraction, within the theory of bit-vectors. Our approach relies on the lazy Satisfiability Modulo Theories (SMT) paradigm. We develop a satisfiability procedure for reasoning about bit vectors that carefully leverages on the power of a Boolean SAT solver to deal with components that are more naturally "Boolean", and activates bit-vector reasoning whenever possible. The procedure has two distinguishing features. First, it relies on the on-line integration of a SAT solver with an incremental and backtrackable solver for BV that enables dynamical optimization of the reasoning about bit vectors; for instance, this is an improvement over static encoding methods which may generate smaller slices of bit-vector variables. Second, the solver for BV is layered (i.e., it privileges cheaper forms of reasoning), and it is based on a flexible use of term rewriting techniques and inference rules. We evaluate our approach on a set of realistic industrial benchmarks, and demonstrate its feasibility with respect to state-of-the-art Boolean satisfiability solvers, as well as other decision procedures for SMT(BV).

Roberto Bruttomesso is a PhD candidate at the University of Trento, Italy (his thesis defense is scheduled on 2/28). During his PhD studies he has been working on SMT solvers, a promising framework that combines SAT and decision procedures for formal verification. He is currently employed at the University of Lugano under the supervision of Prof. Natasha Sharygina. Appointments: dcm@cs.cmu.edu