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:
Use the following reference for citing Beaver:
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 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, and Cygwin. 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.
Beaver accepts QF_BV formulae in SMT-LIB syntax. If you are generating your formulae in CVC/STP format, then you can use CVC3 to convert them to SMT-LIB format. 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. Even in verbose mode, Beaver will print the answer “sat” or “unsat” by itself on a line. You can easily grep it out using patterns ”^sat$”, and ”^unsat$” (or, just single egrep pattern ”^(un)?sat$”).
By default, Beaver uses ABC's internal SAT solver. However, it is not guaranteed to be the most efficient choice. You are strongly encouraged to try out other external SAT solvers using –sat-solver option. 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.