Please note: This PhD seminar will take place online.
Joseph Scott, PhD candidate
David R. Cheriton School of Computer Science
Supervisor: Professor Vijay Ganesh
Solvers for hard combinatorial problems, such as SAT/SMT Solvers, are infamous for underlying worst-case complexity, despite industrial success. For example, the cvc5 SMT solver can solve problems of over a gigabyte in size from certain benchmark families while failing to solve benchmarks that can fit on a single screen. In the latter case, when a competing solver (e.g., z3) solves said benchmark quickly, it suggests the slowdown is caused by programming/solver error rather than the computational complexity of the problem at hand.
To this end, we present two tools. First, BanditFuzz is a performance fuzzer for SMT Solvers. BanditFuzz implements a reinforcement learning loop to find benchmarks where a target solver is slow while a set of relative solvers is fast. BanditFuzz leverages the natural feedback collected from running the solvers to compute a strong reward signal to achieve its goal. Finally, we present Pierce, an upcoming fuzzing tool for neural network verification.