State-of-the-art techniques for automated program verification are required to certify each decision with a formal proof. 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. Synthesis of these proofs necessitates exploring a usually large search space and relies on off-the-shelf constraint solvers. In this talk, I will present new methods that bias the search space with an extensive use of the program's source code. We build on an intuition that the source code often gives useful information, e.g., of occurrences of variables, constants, arithmetic and comparison operators. Thus, we use the source code to automatically construct a formal grammar and iteratively sample the desired proofs from it. We have designed and implemented an extensible verification framework and applied it for proving safety, termination, and non-termination of programs. The experimental evaluation has shown that although the formal grammar is limited to the syntax of the program, in the majority of cases our algorithms are effective and fast.
Grigory Fedyukovich is a postdoc at Princeton University, working with Prof. Aarti Gupta. He completed his PhD at University of Lugano, Switzerland, under supervision of Prof. Natasha Sharygina, and then was a postdoc at University of Washington, Seattle, with Prof. Rastislav Bodik.