SPLASH 2021
Sun 17 - Fri 22 October 2021 Chicago, Illinois, United States
Wed 20 Oct 2021 11:20 - 11:35 at Zurich B - Testing Chair(s): Iulian Neamtiu
Wed 20 Oct 2021 19:20 - 19:35 at Zurich B - Testing - Mirror Chair(s): Steve Blackburn

We propose Generative Type-Aware Mutation, an effective approach for testing SMT solvers. The key idea is to realize generation through the mutation of expressions rooted with parametric operators from the SMT-LIB specification. Generative Type-Aware Mutation is a hybrid of mutation-based and grammar-based fuzzing and features an infinite mutation space—overcoming a major limitation of OpFuzz, the state-of-the-art fuzzer for SMT solvers. We have realized Generative Type-Aware Mutation in a practical SMT solver bug hunting tool, TypeFuzz. During our testing period with TypeFuzz, we reported over 237 bugs in the state-of-the-art SMT solvers Z3 and CVC4. Among these, 189 bugs were confirmed and 176 bugs were fixed. Most notably, we found 18 soundness bugs in CVC4’s default mode alone. Several of them were two years latent (7/18). CVC4 has been proved to be a very stable SMT solver and has resisted several fuzzing campaigns.

Wed 20 Oct

Displayed time zone: Central Time (US & Canada) change

10:50 - 12:10
TestingOOPSLA at Zurich B +8h
Chair(s): Iulian Neamtiu New Jersey Institute of Technology
10:50
15m
Talk
Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic BugsVirtual
OOPSLA
Ting Su East China Normal University, Yichen Yan East China Normal University, Jue Wang Nanjing University, Jingling Sun East China Normal University, Yiheng Xiong East China Normal University, Geguang Pu East China Normal University, Ke Wang Visa Research, Zhendong Su ETH Zurich
DOI
11:05
15m
Talk
Permchecker: A Toolchain for Debugging Memory Managers with TypestateVirtual
OOPSLA
Karl Cronburg Tufts University, Sam Guyer Tufts University
DOI Pre-print
11:20
15m
Talk
Generative Type-Aware Mutation for Testing SMT SolversVirtual
OOPSLA
Jiwon Park École Polytechnique, Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
DOI
11:35
15m
Talk
Programming and Execution Models for Parallel Bounded Exhaustive TestingIn-Person
OOPSLA
Nader Al Awar University of Texas at Austin, Kush Jain University of Texas at Austin, Chris Rossbach University of Texas at Austin; Katana Graph, Milos Gligoric University of Texas at Austin
DOI
11:50
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA

18:50 - 20:10
Testing - MirrorOOPSLA at Zurich B
Chair(s): Steve Blackburn Australian National University
18:50
15m
Talk
Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic BugsVirtual
OOPSLA
Ting Su East China Normal University, Yichen Yan East China Normal University, Jue Wang Nanjing University, Jingling Sun East China Normal University, Yiheng Xiong East China Normal University, Geguang Pu East China Normal University, Ke Wang Visa Research, Zhendong Su ETH Zurich
DOI
19:05
15m
Talk
Permchecker: A Toolchain for Debugging Memory Managers with TypestateVirtual
OOPSLA
Karl Cronburg Tufts University, Sam Guyer Tufts University
DOI Pre-print
19:20
15m
Talk
Generative Type-Aware Mutation for Testing SMT SolversVirtual
OOPSLA
Jiwon Park École Polytechnique, Dominik Winterer ETH Zurich, Chengyu Zhang East China Normal University, Zhendong Su ETH Zurich
DOI
19:35
15m
Talk
Programming and Execution Models for Parallel Bounded Exhaustive TestingIn-Person
OOPSLA
Nader Al Awar University of Texas at Austin, Kush Jain University of Texas at Austin, Chris Rossbach University of Texas at Austin; Katana Graph, Milos Gligoric University of Texas at Austin
DOI
19:50
20m
Live Q&A
Discussion, Questions and Answers
OOPSLA