[FM-India] IARCS Verification Seminar Series -- Talk by Grigory Fedyukovich on August 4, 1900 hrs IST

[Kumar Madhukar]

Dear all,

The Indian Association for Research in Computing Science (IARCS) is pleased to announce a Verification Seminar Series -- a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis.

Please visit the website for more information (upcoming talks, talk videos, meeting details, etc.): https://fmindia.cmi.ac.in/vss/

The first talk in this series will be given by Grigory Fedyukovich, who is an Assistant Professor at Florida State University, USA. The talk is scheduled on Wednesday, August 4, at 1900 hrs IST (details appended below).

The aim of this talk-series is to provide a platform for Formal Methods researchers to interact regularly. In addition, we hope that it will make it easier for researchers to explore newer problems/areas and collaborate on them, and for younger researchers to start working in these areas.

All are welcome to join.


Best regards,
Deepak, Madhukar, Rahul, Srivathsan


=============================================================

Title: Constrained Horn Clauses for Verification and Synthesis

Meeting Link: https://us02web.zoom.us/j/89926920537?pwd=dGMwNjY0TFFJYW1Ocnk0YTUyVjZOUT09
(Meeting ID: 899 2692 0537, Passcode: 414073)

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.

Bio: Dr. 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.


=====-----=====-----=====
Notice: The information contained in this e-mail
message and/or attachments to it may contain 
confidential or privileged information. If you are 
not the intended recipient, any dissemination, use, 
review, distribution, printing or copying of the 
information contained in this e-mail message 
and/or attachments to it are strictly prohibited. If 
you have received this communication in error, 
please notify us by reply e-mail or telephone and 
immediately and permanently delete the message 
and any attachments. Thank you