Fuzzing Symbolic Expressions
Luca Borzacchiello, Emilio Coppa, Camil Demetrescu

TL;DR
This paper introduces FUZZY-SAT, an approximate solver inspired by fuzzing techniques, which effectively checks the satisfiability of symbolic expressions in hybrid fuzzing contexts, offering a competitive alternative to traditional SMT solvers.
Contribution
The paper presents FUZZY-SAT, a novel approximate solver that applies fuzzing-inspired techniques to satisfiability checking, enhancing hybrid fuzzing engines.
Findings
FUZZY-SAT is competitive with Z3 in handling symbolic queries.
FUZZY-SAT complements existing SMT solvers in hybrid fuzzing.
The approach offers a viable alternative to classic SMT solving techniques.
Abstract
Recent years have witnessed a wide array of results in software testing, exploring different approaches and methodologies ranging from fuzzers to symbolic engines, with a full spectrum of instances in between such as concolic execution and hybrid fuzzing. A key ingredient of many of these tools is Satisfiability Modulo Theories (SMT) solvers, which are used to reason over symbolic expressions collected during the analysis. In this paper, we investigate whether techniques borrowed from the fuzzing domain can be applied to check whether symbolic formulas are satisfiable in the context of concolic and hybrid fuzzing engines, providing a viable alternative to classic SMT solving techniques. We devise a new approximate solver, FUZZY-SAT, and show that it is both competitive with and complementary to state-of-the-art solvers such as Z3 with respect to handling queries generated by hybrid…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
