A Lazy and Layered SMT($\mathcal{BV}$) Solver for Hard Industrial Verification Problems

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 paper we advocate reasoning at higher level of abstraction, within the theory of bit vectors ($\mathcal{BV}$), where structural information (e.g. equalities, arithmetic functions) is not blasted into bits.Our approach relies on the lazy Satisfiability Modulo Theories (SMT) paradigm. We developed a satisfiability procedure for reasoning about bit vectors that carefully leverages on the power of 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 ${\mathcal{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 ${\mathcal{BV}}$ is layered (i.e., it privileges cheaper forms of reasoning), and it is based on a flexible use of term rewriting techniques.

We evaluate our approach on a set of realistic industrial benchmarks, and demonstrate substantial improvements with respect to state-of-the-art boolean satisfiability solvers, as well as other decision procedures for SMT${\mathcal{(BV)}}$.

This work has been partly supported by ORCHID, a project sponsored by Provincia Autonoma di Trento, and by a grant from Intel Corporation. The last author would also like to thank the EU project S3MS “Security of Software and Services for Mobile System” contract n. 27004 for supporting part of his research.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.