Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
summary
A solver, Sādhak, couples an SMT engine (built on CVC4) with a fuzzer (AFL++) to handle closed-box functions by compiling expressions to small programs and exchanging partial models and learned conflicts via a CB Theory and a conflict-driven first-loop. The implementation solves 101/107 benchmarks in its CDfL mode, beats the prior tool by 36.45% more benchmarks, shows 5.72× better PAR-2 and 14.62× speedup on common cases, and uses a 600s fuzzer timeout.
AI-written summary · about
chapters (16)
- 0:00Introduction
- 0:41Problem statement
- 2:10Tool Sadaf
- 2:51Contributions
- 3:34CDFL algorithm overview
- 5:01Algorithm example
- 7:15Fuzzer inputs from constraints
- 8:24Comparison with Delphi and Colossus
- 9:50Evaluation results
- 10:31Conclusion and artifacts
- 11:15Q&A session part one
- 13:43Q&A session part two
- 15:52Q&A session part three
- 17:39Q&A session part four
- 19:45Q&A session part five
- 21:18Engineering choices
related talks
13mOn the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers
35mA Peek Inside SAT Solvers
16mQuteFuzz: Fuzzing quantum compilers using randomly generated circuits with control(…)
40mReasoning Under Uncertainty in SMT Solving, Research, and Life
15mInterleaving Large Language Models for Compiler Testing
13mProgram Analysis via Efficient Symbolic Abstraction
35mThe Mastermind behind Refinement Types
18mScalable Floating-Point Satisfiability via Staged Optimization