Beaver Bit-vector Decision Procedure

Beaver is a Satisfiability Modulo Theories (SMT) decision procedure for the theory of quantifier-free finite-precision bit-vector arithmetic ( [http://combination.cs.uiowa.edu/smtlib/logics/QF_BV.smt QF_BV] ). Its prototype implementation 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), computer security (rich in nonlinear arithmetic) and formal equivalence checking (rich Boolean structure).

Beaver Decision Procedure Algorithm

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 problem in conjunctive normal form (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 logic synthesis to perform Boolean simplifications on the AIG before translating the AIG to CNF. Any off-the-shelf SAT solvers () can then be used on the CNF formula.

Authors

* [http://www.eecs.berkeley.edu/~jha Susmit Jha]
* Rhishikesh Limaye
* [http://www.eecs.berkeley.edu/~sseshia/ Sanjit Seshia]

Prototype Availability and Usage

Source code for Beaver is distributed under [http://www.opensource.org/licenses/bsd-license.php BSD license] . This prototype was placed third in the QF_BV category of the [http://www.smtcomp.org/ SMT competition] 2008. It was ranked first among open source QF_BV SMT solvers. See [http://www.smtexec.org/exec/divisionResults.php?jobs=311&division=QF_BV results] . Complete description of the algorithm and prototype tool is available at [http://www.eecs.berkeley.edu/~jha/beaver.html Beaver website] . For more details, visit the [http://uclid.eecs.berkeley.edu/wiki/index.php/Main_Page UCLID group webpage] ] . Current implementation accepts QF_BV formulae in [http://combination.cs.uiowa.edu/smtlib/papers.html SMT-LIB standard Version 1.2] with limited backward compatibility with earlier versions.