[  discussion | download | license ]

VoteSMT is a parallel majority voting framework that can be used to find failure-inducing benchmarks for SMT solvers, e.g. benchmarks that cause crashes, infinite loops or incorrect results. It uses the fuzzer FuzzSMT in order to generate random SMT benchmarks. Discrepancies between solvers, i.e. some solvers report sat while the other solvers report unsat, are automatically classified as correct resp. incorrect by the majority voting principle. An earlier version of VoteSMT has been used for the experiments in our paper Fuzzing and Delta-Debugging SMT Solvers.

See the README for more information and a mini tutorial.

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

[ votesmt-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.