[  download | overview | publications | license ]

Download

• Source code is available from the project webpage of QBFuzz.

Overview

QBFuzz is a fuzzer for quantified boolean formulae in QDIMACS format. It generates random QBFs with respect to certain parameters such as number of variables, number of clauses, min/max clause length etc. QBFuzz does not use fixed parameter values but rather ranges of values, which potentially increases diversity of generated formulae. When combined with delta-debugging, QBFuzz can be effectively used for automated testing of QBF solvers. The idea is to rapidly feed a QBF solver with random formulae in order to trigger "rare" bugs (e.g. corner cases, complex data structures) which might remain undetected using techniques such as unit tests. See also the README file for further information.

Publications

Paper and talk at SAT'10.

License

QBFuzz was developed by Mathias Preiner as a bachelor project. It is released under GNU GPLv3. See also file COPYING that is part of the distribution.