Fuzzing and Delta-Debugging Tools

News

New only partially grammar-aware fuzzer and delta-debugging tool set ddsexpr for s-expressions.

New ddSMT delta-debugger for SMTLIB 2.0.

SAT Tools

The tool suite CNFuzzDD contains a layered CNF fuzzer and both a sequential and a multithreaded delta debugger.

FuzzSAT is a fuzzer which generates structured CNFs.

3SATGen is a generator for random 3-SAT formulae.

QBF Tools

QBFuzz is a fuzzer which generates random QBFs.

QBFDD is a delta-debugger for QBFs in QDIMACS format.

BlocksQBF is a generator for QBFs according to a random model.

Answer Set Programming (ASP) Tools

FuzzASP is a fuzzer that can be used to generate random answer set programs.

DeltaASP is a delta-debugger which is able to to automatically minimize failure-inducing answer set programs in the syntax of lparse.

Satisfiability Modulo Theories (SMT) Tools

New ddSMT delta-debugger for SMTLIB 2.0.

FuzzSMTBV is a light-weight fuzzer that can be used to generate random SMT benchmarks with bit-vectors and arrays.

FuzzSMT is a more sophisticated SMT fuzzer that supports almost all relevant logics of the SMT-LIB.

DeltaSMT is a delta-debugger which is able to to automatically minimize failure-inducing SMT benchmarks. It can be particularly useful in the process of debugging SMT solvers.

VoteSMT is a parallel majority voting framework for SMT solvers. It can be used to find and classify failure-inducing SMT benchmarks.