Beaver is an SMT solver (decision procedure) for the theory of quantifier-free finite-precision bit-vector arithmetic (QF_BV). It supports all operators defined under QF_BV, including signed and unsigned non-linear arithmetic operators. Beaver is specially adapted for solving SMT formulae arising out of program analysis (rich in conjunction of linear constraints such as path feasibility queries), security (rich in nonlinear arithmetic) and equivalence checking (rich Boolean structure). Beaver operates by performing a series of rewrites and simplifications that transform the starting bit-vector arithmetic formula into a Boolean circuit and then into a Boolean satisfiability (SAT) problem in CNF. The main transformations performed by Beaver include: - Constant propagation and constraint propagation: Beaver uses an event-driven approach to propagate constants and constraints through the formula to simplify it. A simple form of constraint that appears in many software benchmarks is an equality that uses a fresh variable to name an expression. Both backward and forward propagation are performed. - Number theoretic rewrite rules: Beaver also uses number-theoretic and other word-level rewrite rules to simplify the formula. These interact with the above step by creating new opportunities for constant/constraint propagation. - Boolean simplifications using synthesis techniques: instead of directly bit-blasting the formula to CNF, Beaver first creates an And-Inverter Graph (AIG) representation of the formula, and then uses the ABC logic synthesis engine to perform Boolean simplifications on the AIG before translating the AIG to CNF. Any off-the-shelf SAT solver (either CNF-based or circuit-based) can then be used to solve the resulting CNF/AIG formula.

Use the following reference for citing Beaver:

Susmit Jha, Rhishikesh Limaye, and Sanjit Seshia. Beaver: Engineering an efficient SMT solver for
bit-vector arithmetic. In Computer Aided Verification, pages
668-674. 2009. DOI

BibTeX:

@incollection{jha2009beaver, author = {Jha, Susmit and Limaye, Rhishikesh and Seshia, Sanjit}, booktitle = {Computer Aided Verification}, doi = {10.1007/978-3-642-02658-4_53}, journal = {Lecture Notes in Computer Science}, pages = {668--674}, title = {Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic}, url = {http://dx.doi.org/10.1007/978-3-642-02658-4_53}, year = {2009}, }

- Beaver placed third in the QF_BV category of the SMT competitions in 2008 and 2009. It was ranked first among open source QF_BV SMT solvers. See results.

Susmit Jha (For any assistance, comment or suggestions contact: last-name@eecs.berkeley.edu where last-name = jha)

Rhishikesh Limaye

Advisor: Professor Sanjit Seshia

Beaver is available as open source under the BSD license (see license). Apart from source code, we also provide binary distributions for Linux 32-bit, 64-bit. Please tell us about yourself before going to the download page. We use the information below to know who is interested in our solver and for what application. Name and email are required.

For compilation from source, you need OCaml. A fairly recent version, say 3.09, 3.10, 3.11, should work. Note: Cygwin's default OCaml package won't work probably, as it seems too old currently -- 3.08. Specifically, it lacks the executable ## How to use

## Acknowledgment

## Links

`camlp4of`

, which will produce an error during configure stage. You can try removing that check, by editing `acinclude.m4`

, because we don't really use `camlp4of`

, but we don't know if there are any other things missing in OCaml 3.08.
You should also have the following standard packages of OCaml.

The best way to get these packages is by installing OCaml using the GODI distribution, and then using its `godi_console`

to get the packages. Or some Linux distributions have pre-built packages for these. Or, you can install them manually by downloading their sources from the respective websites.

As GNU autotools are used, compilation involves running `configure`

followed by `make; make install`

. There is one caveat: **in-place compilation doesn't work, i.e. ./configure; make won't work**. Instead, you should use a build directory that is different from the source directory. The following set of commands is most likely to work (I've tested them on Linux and Cygwin).

tar zxf <package.tar.gz> cd <package> mkdir build cd build ../configure make make install

Beaver accepts QF_BV formulae in SMT-LIB syntax. The formula can be piped into stdin, or provided as a single file argument. By default Beaver runs in silent mode conforming to SMTCOMP standard. It only outputs "sat" or "unsat" on stdout. Use "-verbose" flag to make it print details of different steps of solving. Any external SAT solver (CNF or AIG) can be used as a back-end of Beaver using "-sat-solver" option which over-rides the default SAT solver. Any CNF- or AIG- based SAT solver that conforms to SAT competition requirements works. Beaver automatically detects whether the solver specified with "-sat-solver" is a CNF- or AIG- based solver.

We are thankful to Bryan Brady for his suggestions and for his help in generating hardware benchmarks. We also thank Robert Brayton and Alan Mishchenko for helping us in using ABC. We are also thankful to Dawn Song, David Wagner and David Molnar for providing us with software benchmarks to test and improve our SMT solver.

Website maintained at UC Berkeley