Beaver is a Satisfiability Modulo Theories (SMT) decision procedure for the theory of quantifier-free finite-precision bit-vector arithmetic (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 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:
Source code for Beaver is distributed under BSD license This prototype was placed third in the QF_BV category of the SMT competition 2008. It was ranked first among open source QF_BV SMT solvers. See results Complete description of the algorithm and prototype tool is available at Beaver website For more details, visit the UCLID group webpage]. Current implementation accepts QF_BV formulae in SMT-LIB standard Version 1.2 with limited backward compatibility with earlier versions.