[  discussion | download | license ]

FuzzSMTBV is a light-weight grammar-based blackbox fuzzing tool that can be used to generate random SMT benchmarks in order to fuzz-test SMT solvers. FuzzSMTBV is our first fuzzer prototype for SMT and is limited to bit-vectors and arrays. Note that we also developed FuzzSMT, which is a sophisticated fuzzer that supports more theories and provides more features. An earlier version of FuzzSMTBV has been used for the experiments in our paper Fuzzing and Delta-Debugging SMT Solvers.

See the README for more information about FuzzSMTBV.

Discussion Platform

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.

Download

[ fuzzsmtbv-0.1.tar.bz2 ]

Version 0.1 is the first public release.

License

We use the GPL license version 3. The license can be found in the file COPYING which comes with the tool.