Beaver: An SMT Solver for Bit-Vector Arithmetic
 

Beaver has been released under BSD license and is now maintained at here. This page is now history! :)

And yes, I am still interested in decision procedures and your feedbacks, suggestions and criticisms are welcome. In particular, do drop me a mail if you try Beaver out and find it awfully bad for your application. If possible also send me any example that chokes Beaver. Though it is open source and you can always tune it yourself, I might still have advantage of familarity with code.

----------------------------------------------------------------------------------------

Overview

Beaver is an SMT solver (theorem prover) for the theory of quantifier-free finite-precision bit-vector arithmetic. 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).

The development of Beaver started as my summer project with Professor Sanjit Seshia in May 2007. The main goal was to develop a state-of-the-art theorem prover for bit-vector logic which could take place of the decision procedure in UCLID verification system. The key research challenges were to develop an efficient technique to handle nonlinear arithmetic as well as to handle bit-vector formulae rich in Boolean structure. I continued to work on it as my course projects in Fall, 2007. Rhishi joined us in December 2007 and the final prototype tool was finished with all its optimizations in Spring 2008. Beaver participated in SMTCOMP 2008 and results are available at here .

Acknowledgment

I am thankful to Professor Sanjit Seshia for his support and insightful suggestions. I am also thankful to Rhishi who helped me in developing Beaver. I am also grateful to Bryan Brady who actively participated in many discussions. I express my gratitude to Professor Robert Brayton and Alan Mishchenko for helping us in using ABC as well as providing us with many interesting suggestions. I am thankful to David Wagner, David Molnar and Dawn Song for providing us with a number of benchmarks from security. I am also grateful to Professor Priyank Kalla for providing us with data-path equivalence checking benchmarks.

Back to Homepage.