124
IRUS Total
Downloads

© 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.

File Description SizeFormat 
main.pdfAccepted version663.41 kBAdobe PDFView/Open
Title: © 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.
Authors: Liew, D
Cadar, C
Donaldson, A
Stinnett, JR
Item Type: Conference Paper
Abstract: 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.
Issue Date: Aug-2019
Date of Acceptance: 24-May-2019
URI: http://hdl.handle.net/10044/1/72043
DOI: 10.1145/3338906.3338921
Publisher: ACM
Start Page: 521
End Page: 532
Copyright Statement: This paper is embargoed until publication.
Sponsor/Funder: Engineering & Physical Science Research Council (EPSRC)
Engineering & Physical Science Research Council (EPSRC)
Funder's Grant Number: EP/I012036/1
EP/N007166/1
Conference Name: ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE ’19)
Keywords: Science & Technology
Technology
Computer Science, Software Engineering
Computer Science
Constraint solving
feedback-directed fuzzing
SYMBOLIC EXECUTION
Publication Status: Published
Start Date: 2019-08-26
Finish Date: 2019-08-30
Conference Place: Tallinn, Estonia
Online Publication Date: 2019-08
Appears in Collections:Computing
Faculty of Engineering