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.