Beaver bit-vector decision procedure

{| align="right"
| __TOC__
|}

In [[mathematical logic]] and [[computability theory]], '''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 ([[:Category: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.

[[Category:Automated theorem proving]]
[[Category:SMT solvers]]
[[Category:Constraint satisfaction]]
[[Category:Number theory]]
[[Category:Modular arithmetic]]
[[Category:Finite fields]]
[[Category:Formal methods]]
[[Category:Free theorem provers]]