Data e hora: terça, 5 de setembro de 2023, às 16h
Local: sala 6321 (DCC)
Palestrante: Dr. Grigory Fedyukovich (Florida State University)
Abstract: To guarantee the absence of program bugs, state-of-the-art techniques synthesize proofs that are returned to users and can be validated. Proofs need to be generated automatically by algorithms that deal with logic formulas over a set of unknown predicates, also known as Constrained Horn Clauses (CHCs). CHCs have lately become the language for problems in program verification, and they offer the advantages of flexibility and modularity in designing verifiers for various systems and languages. In this talk, I will overview some new methods for program verification that take systems of CHCs as input and apply a CHC solver to generate proofs. 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: using static analysis, it identifies ranges of elements accessed in each loop, and then it learns useful facts about individual elements and generalizes them to entire ranges, which is often sufficient to conclude proofs. The presented approach is implemented in a tool called FreqHorn that effectively exploits state-of-the-art constraint solvers. We have experimentally demonstrated the tool’s effectiveness, efficiency, and quality of generated proofs on ranges of benchmarks.
Bio: Dr. Grigory Fedyukovich is an Assistant Professor at Florida State University and a Visiting Academic at Amazon. He completed his Ph.D. at the University of Lugano under the supervision of Prof Natasha Sharygina and then a postdoc at the University of Washington with Prof Rastislav Bodik and at Princeton University with Prof Aarti Gupta. His main research interests are in the fields of automated reasoning, software verification, and synthesis.
