USI - Email

Archive / INF Seminars / INF_2019_07_29_Grigory_Fedyukovich

USI - Email

	Quantified Invariants via Syntax-Guided Synthesis

Host: Prof. Natasha Sharygina

Monday

29.07

USI Lugano Campus, room SI-003, Informatics building

10:30-11:30


	Grigory Fedyukovich Florida State University, USA

Abstract:
To guarantee the absence of bugs in programs, state-of-the-art techniques synthesize checkable proofs such as inductive invariants, ranking functions, and recurrence sets. 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 extensive use of the program's source code. Intuitively, 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.

For programs handling arrays, proofs are likely to contain universally quantified formulas, which are difficult to find, and difficult to prove inductive. I will present an algorithm that discovers quantified invariants in stages. First, by exploiting the program syntax, it identifies ranges of elements accessed in each loop. Second, it identifies potentially useful facts about individual elements and generalizes them to hypotheses about entire ranges. Finally, by applying recent advances of SMT solving, the algorithm filters out wrong hypotheses. The combination of properties is often enough to prove that the program meets a safety specification. The algorithm has been implemented in a solver for Constrained Horn Clauses, called FreqHorn, and extended to deal with multiple (possibly nested) loops. We show that FreqHorn advances state-of-the-art on a wide range of public array-handling programs.

Biography:
Prof. Dr. Grigory Fedyukovich is an Assistant Professor at Florida State University, USA. He completed his Ph.D. at the Università della Svizzera italiana (USI), Switzerland, under the supervision of Prof. Natasha Sharygina, and then he was a postdoc at the University of Washington with Prof. Rastislav Bodik and at Princeton University with Prof. Aarti Gupta. His research interests are in software verification and synthesis, program equivalence, and applications of relational verification to analyzing software security.