SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Sat 10 Dec 2022 14:00 - 14:30 at AMRF Auditorium - Testing and Maintenance Chair(s): Işıl Dillig

Programming languages and software engineering tools routinely encounter components that are difficult to reason on via formal techniques or whose formal semantics are not even available—third-party libraries, inline assembly code, SIMD instructions, system calls, calls to machine learning models, etc. However, often access to these components is available as input-output oracles—interfaces are available to query these components on certain inputs to receive the respective outputs. We refer to such functions as \textit{closed-box functions}. Regular SMT solvers are unable to handle such closed-box functions.

We propose Sādhak, a solver for SMT theories modulo closed-box functions. Our core idea is to use a synergistic combination of a fuzzer to reason on closed-box functions and an SMT engine to solve the constraints pertaining to the SMT theories. The fuzz and the SMT engines attempt to converge to a model by exchanging a rich set of \textit{interface constraints} that are relevant and interpretable by them. Our implementation, Sādhak, demonstrates a significant advantage over the only other solver that is capable of handling such closed-box constraints: Sādhak solves 36.45$%$ more benchmarks than the best-performing mode of this state-of-the-art solver and has 5.72x better PAR-2 score; on the benchmarks that are solved by both tools, Sādhak is (on an average) 14.62x faster.

Sat 10 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
Testing and MaintenanceOOPSLA at AMRF Auditorium
Chair(s): Işıl Dillig University of Texas at Austin
13:30
30m
Talk
Overwatch: Learning Patterns in Code Edit Sequences
OOPSLA
Yuhao Zhang University of Wisconsin-Madison, Yasharth Bajpai Microsoft, Priyanshu Gupta Microsoft, Ameya Ketkar Uber, Miltiadis Allamanis Microsoft Research, Titus Barik Microsoft, Sumit Gulwani Microsoft, Arjun Radhakrishna Microsoft, Mohammad Raza Microsoft, Gustavo Soares Microsoft, Ashish Tiwari Microsoft
DOI
14:00
30m
Talk
Satisfiability Modulo Fuzzing: A Synergistic Combination of SMT Solving and Fuzzing
OOPSLA
Sujit Kumar Muduli IIT Kanpur, Subhajit Roy IIT Kanpur
DOI
14:30
30m
Talk
Synthesizing Code Quality Rules from Examples
OOPSLA
DOI