Colloquium - Synthesizing Proofs for Program Verification

Date: 
March 6, 2019 - 3:30pm to 4:30pm
Location: 
2217 SC
Speaker: 
Grigory Fedyukovich
Princeton University | Computer Science Department

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 to automated reasoning, we hope to get more trustworthy, secure, and efficient programs; and 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 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 an extensible verification framework called FreqHorn that is 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

Grigory Fedyukovich - Princeton profileDr. 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.