Special Seminar: Grigory Fedyukovich "Synthesizing Proofs for Program Verification"

Synthesizing Proofs for Program Verification

Grigory Feduykovich

Abstract:

Software controls every device, system, and infrastructure serving our society. The rapid growth of complexity and high demand for human resources makes the task of building software tedious and error-prone. With techniques for automated reasoning, we expect to receive more trustworthy, secure, and efficient programs. In this talk, I will overview how such techniques can be built on top of solvers for Satisfiability Modulo Theories (SMT). SMT-based tools not only reveal bugs in programs but also synthesize proofs that no bugs can ever occur. In particular, when verifying program safety, a proof is an inductive invariant; when proving program termination, a proof is a ranking function; and when proving program non-termination, a proof is a recurrence set. SMT-based synthesis of these proofs necessitates exploring a usually large search space, which however can be pruned using the program's source code. I will present a verification framework, called FreqHorn, that is extensible, scalable and fast while solving a wide range of practical verification tasks. FreqHorn enables a broader class of applications, and in the future, it will help push the frontiers in automated program repair, functional synthesis, and security verification.

Bio:

Dr. Grigory Fedyukovich is a postdoc at Princeton University, working with Prof Aarti Gupta. He completed his Ph.D. at the University of Lugano, Switzerland, under the supervision of Prof Natasha Sharygina, and then he was a postdoc at the University of Washington, with Prof Rastislav Bodik. His research interests are in software verification and synthesis, program equivalence, and applications of relational verification to analyzing software security.