Title: Analysis of incomplete programs via Proof Engines and Fuzzing

Speaker: Subhajit Roy    (bio) (bio)

Subhajit Roy is an Associate Professor in the Department of Computer Science and Engineering at IIT Kanpur. His research is aimed at designing new algorithms and developing automated tools for analysis, verification, optimization, synthesis, debugging, and interpreting both (conventional) programs as well as for machine learnt models, using formal methods (logic, automata theory, compiler design) and data-driven techniques (machine learning, artificial intelligence, statistics).

When: Tuesday, 10 October 2023 at 1900 hrs (IST)       

Abstract:
We tackle the problem of testing and verifying "incomplete" programs — that contain components whose source code is either unavailable (like third-party libraries and cloud-based APIs), or too complex to model formally (like large machine learning models). We show how classical techniques like symbolic execution, deductive verification and SMT solving can be "lifted" to this setting. The techniques essentially employ a combination of automated SMT based proofs, with tests from modern fuzzers for testing and "almost" verification of such programs. We will delve into one of our contributions: 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 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.