The Just Fuzz It (JFS) solver is based on coverage-guided fuzzing for determining the satisfiability of SMT constraints, particularly those that involve floating-point arithmetic.

JFSampler is an SMT sampler built on top of JFS; JFSampler can find a large number of solutions for a satisfiable formula.

Overview

JFS

We investigate the use of coverage-guided fuzzing as a means of proving satisfiability of SMT formulas over finite variable domains, with specific application to floating-point constraints. We show how an SMT formula can be encoded as a program containing a location that is reachable if and only if the program’s input corresponds to a satisfying assignment to the formula. A coverage-guided fuzzer can then be used to search for an input that reaches the location, yielding a satisfying assignment. We have implemented this idea in a tool, Just Fuzz-it Solver (JFS), and we present a large experimental evaluation showing that JFS is both competitive with and complementary to state-of-the-art SMT solvers with respect to solving floating-point constraints, and that the coverage-guided approach of JFS provides significant benefit over naive fuzzing in the floating-point domain. Applied in a portfolio manner, the JFS approach thus has the potential to complement traditional SMT solvers for program analysis tasks that involve reasoning about floating-point constraints.

JFSampler

SMT sampling involves finding numerous satisfying assignments (samples), for an SMT formula, and is increasingly finding applications in software testing. An effective SMT sampler should achieve high throughput, yielding a large number of samples in a given time budget, and high diversity, yielding samples that cover disparate parts of the solution space.

Most SMT samplers rely on off-the-shelf SMT solvers and thus inherit those solvers’ scalability issues. Because SMT solvers tend to scale poorly when applied to floating-point constraints, the scalability and diversity of SMT sampling is correspondingly limited in the floating-point domain.

We propose JFSampler, the first SMT sampling technique built on top of coverage-guided fuzzing. JFSampler extends Just Fuzz-it Solver (JFS), a scalable but incomplete SMT solver that is effective at finding solutions to floating-point formulas by encoding satisfiability as a reachability problem that is then offloaded to a fuzzer. By building on JFS, JFSampler has an advantage over other SMT samplers in the floating-point domain. Further, we propose two novel strategies that increase both throughput and diversity of sampled solutions. First, JFSampler enhances the fuzzer’s code coverage feedback signal by measuring coverage of the formula’s solution space. Second, JFSampler incorporates a custom mutator tailored for SMT sampling. By design, these two novel techniques can be combined, having a positive synergy on throughput and diversity.

We present a large evaluation over QF_FP and QF_BVFP formulas from the SMT-LIB benchmark. Our results show that JFSampler achieves substantial improvements over SMTSampler, a state-of-the-art SMT sampling technique, when applied to floating-point formulas.

Artefact

The code for JFS is available here, and for JFSSampler is available here.

Research Support

JFS

This research was supported in part by the UK EPSRC via grants EP/N007166/1, EP/P010040/1 and EP/R006865/1.

JFSampler

This research has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation program (grant agreement 819141).

Publications

• Scalable SMT Sampling for Floating-point Formulas via Coverage-guided Fuzzing

  Manuel Carrasco, Cristian Cadar, Alastair Donaldson

  IEEE International Conference on Software Testing, Verification, and Validation (ICST 2025)

• Just Fuzz It: Solving Floating-point Constraints Using Coverage-guided Fuzzing

  Daniel Liew, Cristian Cadar, Alastair Donaldson, J. Ryan Stinnett

  European Software Engineering Conference / ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE 2019)