An approach based on coverage-guided fuzzing for determining the satisfiability of SMT constraints, particularly those that involve floating-point arithmetic.

Overview

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.

Artefact

The code for JFS is available here.

Research Support

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

Publications

• 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)