Beaver

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.

Reference

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}, } 

News

Authors

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

Download

Total Number of Downloads:

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.

Name:
Email:
Institution:
Purpose:

Installation

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 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

How to use

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.

Acknowledgment

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.

Links

Beaver License
Course Assignment on Beaver
Experimental results for CAV09 paper



Website maintained at UC Berkeley