Boolector

News

Source code release of Boolector 1.4 under GPL.

Launched Google group.

Download

The latest version is available under the GNU General Public License Version 3:

[ boolector-1.4-ffc2089-100608.tar.gz | boolector-1.3-e71a070-100601.tar.gz ]

The second source code release of Boolector 1.4 only fixes some minor issues. You find more information in the NEWS and README files.

Older versions

The latest binary release of Boolector, Boolector 1.2, can be downloaded from the competitor overview of the latest SMT competition.

These are all 32-bit statically linked Linux-x86 binaries. We do not support other platforms at this moment. A source release is not planned either. Finally, the restrictions of the license section apply.

Overview

Boolector is an SMT solver for bit-vectors and arrays. Version 0.0 was used in experiments that are described in our recent SMT'08 paper. Version 0.4 entered the SMT'08 competition and is available from the overview of competitors. It won first places in both the bit-vector (QF_BV) and bit-vector with arrays track (QF_AUFBV). See www.smtcomp.org/2008 for more details. In the latest SMT competition, Boolector 1.2 won the second place in QF_BV and again the first place in QF_AUFBV.

A small history of Boolector can be found in the NEWS file.

Currently, we are working on papers that describe and evaluate Boolector's under-approximation features.

Community

Please use our google group for any questions, bug reports and comments. You should also join if you want to be informed of new releases.

Publications related to Boolector

R. Brummayer. Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays. Ph.D. thesis, Johannes Kepler University Linz, Austria, November 2009.
R. Brummayer, A. Biere. Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In Proc. 15th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'09), Lecture Notes in Computer Science (LNCS), vol. 5505, Springer 2009.
R. Brummayer, A. Biere, F. Lonsing. BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking. In Proc. 1st Intl. Workshop on Bit-Precise Reasoning (BPR'08), Princeton, New Jersey, USA, July 2008.
R. Brummayer, A. Biere. Lemmas on Demand for the Extensional Theory of Arrays. In Proc. 6th Intl. Workshop on Satisfiability Modulo Theories (SMT'08), Princeton, New Jersey, USA, July 2008.
A. Vida. Random Test Case Generation and Delta Debugging for BitVector Logic with Arrays. Master Thesis, Johannes Kepler University, Oct. 2008 (software).

Slides related to Boolector

Boolector 1.2, SMT-COMP'09, Montreal, Canada
Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays, TACAS'09, York, UK
Effective Bit-Width and Under-Approximation, Eurocast'09, Las Palmas de Gran Canaria, Spain
BTOR: Bit-Precise Modelling of Word-Level Problems for Model Checking, BPR'08, Princeton, New Jersey, USA
Lemmas on Demand for the Extensional Theory of Arrays, SMT'08, Princeton, New Jersey, USA
Boolector 0.4, SMT-COMP'08, Princeton, New Jersey, USA
Offline SMT for Arrays, AVM'08, Semmering, Austria

License

Boolector is copyrighted 2007 - 2010 by Robert Brummayer, Armin Biere, Institute for Formal Models and Verification, Johannes Kepler University, Linz, Austria.

The older binary releases until and including Boolector 1.2 are available for research and evaluation purposes in an academic environment only. They can not be used in a commercial environment, particularly as part of a commercial product, without written permission.

For the newer source code releases, starting with Boolector 1.3, we use the GNU General Public License Version 3 (GPLV3). You can find more information about GPLV3 in the file COPYING that comes with the sources. In particular, this license forbids to link or use Boolector 1.3 in a redistributed program, without making the source code of that program available under GPL as well.

In general, Boolector is provided as is, without any warranty.

Please contact Armin Biere for additional questions regarding licensing Boolector under a different license or to obtain more up-to-date versions.