Title: Constrained Horn Clauses for Verification and Synthesis

Speaker: Grigory Fedyukovich    (bio) (bio)

Grigory Fedyukovich is an Assistant Professor at Florida State University, USA. 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 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.

When: Wednesday, 04 August 2021 at 1900 hrs (IST)    

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 (CHC). CHC 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 new methods for solving CHC and applying it in program verification, equivalence checking, and specification synthesis.

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. For proving equivalence between programs handling recursive data types and arrays, I will present an algorithm to generate recursively-defined relational invariants. The approach is based on encoding two programs into a "product CHC" and finding solutions by lifting the constraints from joint methods of the two programs to the base or inductive cases of the recursive invariant. Lastly, I will present a technique for finding maximal and non-vacuous function specifications that learns them simultaneously with learning invariants. The iterative algorithm lazily generalizes non-vacuous specifications in a counterexample-guided loop.

The presented approaches are implemented in the tools sharing the extensible FreqHorn infrastructure that allows to effectively exploit state-of-the-art constraint solvers. We have experimentally demonstrated the tools' effectiveness, efficiency, and the quality of generated proofs on ranges of benchmarks.