Publications

BibTex format

@inproceedings{Liew:2019:10.1145/3338906.3338921,
author = {Liew, D and Cadar, C and Donaldson, A and Stinnett, JR},
doi = {10.1145/3338906.3338921},
pages = {521--532},
publisher = {ACM},
title = {Just fuzz it: solving floating-point constraints using coverage-guided fuzzing},
url = {http://dx.doi.org/10.1145/3338906.3338921},
year = {2019}
}

Download

RIS format (EndNote, RefMan)

TY  - CPAPER
AB  - We investigate the use of coverage-guided fuzzing as a means ofproving satisfiability of SMT formulas over finite variable domains,with specific application to floating-point constraints. We show howan SMT formula can be encoded as a program containing a locationthat is reachable if and only if the program’s input corresponds toa satisfying assignment to the formula. A coverage-guided fuzzercan then be used to search for an input that reaches the location,yielding a satisfying assignment. We have implemented this ideain a tool,JustFuzz-itSolver (JFS), and we present a large experi-mental evaluation showing that JFS is both competitive with andcomplementary to state-of-the-art SMT solvers with respect tosolving floating-point constraints, and that the coverage-guidedapproach of JFS provides significant benefit over naive fuzzing inthe floating-point domain. Applied in a portfolio manner, the JFS approach thus has the potential to complement traditional SMTsolvers for program analysis tasks that involve reasoning aboutfloating-point constraints.
AU  - Liew,D
AU  - Cadar,C
AU  - Donaldson,A
AU  - Stinnett,JR
DO  - 10.1145/3338906.3338921
EP  - 532
PB  - ACM
PY  - 2019///
SP  - 521
TI  - Just fuzz it: solving floating-point constraints using coverage-guided fuzzing
UR  - http://dx.doi.org/10.1145/3338906.3338921
UR  - https://dl.acm.org/doi/10.1145/3338906.3338921
UR  - http://hdl.handle.net/10044/1/72043
ER  -

Download

ProfessorAlastairDonaldson

Contact

Location

Summary

Citation

BibTex format

RIS format (EndNote, RefMan)