ICST 2025
Mon 31 March - Fri 4 April 2025 Naples, Italy
Wed 2 Apr 2025 11:30 - 11:45 at Room A1 - Fuzzing and Security Chair(s): Serge Demeyer

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.

Wed 2 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:30
Fuzzing and SecurityResearch Papers / Industry / Journal-First Papers at Room A1
Chair(s): Serge Demeyer University of Antwerp and Flanders Make vzw
11:00
15m
Talk
SPIDER: Fuzzing for Stateful Performance Issues in the ONOS Software-Defined Network Controller
Research Papers
Ao Li Carnegie Mellon University, Rohan Padhye Carnegie Mellon University, Vyas Sekar Carnegie Mellon University
11:15
15m
Talk
Mutation-based Fuzzing of the Swift Compiler With Incomplete Type Information
Research Papers
Sarah Canto Hyatt University of California, Santa Barbara, Kyle Dewey California State University, Northridge
11:30
15m
Talk
Scalable SMT Sampling for Floating-point Formulas via Coverage-guided Fuzzing
Research Papers
Manuel Carrasco Imperial College London, Cristian Cadar Imperial College London, Alastair F. Donaldson Imperial College London
11:45
15m
Talk
Introducing Black-Box Fuzz Testing for REST APIs in Industry: Challenges and Solutions
Industry
Andrea Arcuri Kristiania University College and Oslo Metropolitan University, Alexander Poth Volkswagen AG, Olsi Rrjolli Volkswagen AG
12:00
15m
Talk
Compiler Fuzzing in Continuous Integration: a Case Study on Dafny
Industry
Karnbongkot Boonriong Imperial College London, Stefan Zetzsche Amazon Web Services, Alastair F. Donaldson Imperial College London
12:15
15m
Talk
Automated SC-MCC Test Case Generation using Coverage Guided Fuzzing
Journal-First Papers
Golla Monika Rani , Sangharatna Godboley National Institute of Technology Warangal
:
:
:
: