[FM-India]IARCS Verification Seminar Series -- Talk by Madhusudan Parthasarathy on Nov. 28 at 1900 hrs IST

Dear all, The next talk in the IARCS Verification Seminar Series will be given by Madhusudan Parthasarathy, a Professor of Computer Science at the University of Illinois at Urbana-Champaign. The talk is scheduled on Tuesday, Nov. 28, at 1900 hrs IST (add to Google calendar <https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=MzViZ3N0anUwOTVxYzBmZzU3ODFla2Q3YTQgdnNzLmlhcmNzQG0&tmsrc=vss.iarcs%40gmail.com> ). The details of the talk can be found on our webpage ( https://fmindia.cmi.ac.in/vss/), and also appended to the body of this email. The Verification Seminar Series, an initiative by the Indian Association for Research in Computing Science (IARCS), is a monthly, online talk-series, broadly in the area of Formal Methods and Programming Languages, with applications in Verification and Synthesis. 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, Akash, Deepak, Madhukar, Srivathsan ============================================================= Title: Learning Logical Expressions Meeting Link: https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09 (Meeting ID: 891 6409 4870, Passcode: 082194) Abstract: We consider the problem of learning logical formulas/expressions that work as classifiers of structures. Logic learning has many applications ranging from program synthesis from input-output examples, learning specifications from code (contracts and inductive invariants), interpretable concept learning in AI, synthesizing lemmas to help prove theorems, finding axiomatizations, and, more generally, replacing certain creative tasks that currently require human help in many applications. We will first motivate logic learning using the applications above. We then will turn a theory lens to this problem by considering when the logic learning problem is *decidable*. We show a general technique using tree automata that realize learning algorithms for a variety of logics/languages ranging from fragments of FOL, regular expressions, temporal logics, grammars, to string transformation for Excel (as in Flashfill). We in fact will show a *meta-theorem* that can be used to show a logic is decidable simply by programming a particular kind of evaluator for its semantics. This theory suggests that many logics can be learned by using Version Space Algebras (VSAs) based on tree automata. If time permits, we will also consider the problem of learning logics themselves to aid few-shot learning. Bio: Madhusudan Parthasarathy is a Professor of Computer Science at the University of Illinois at Urbana-Champaign. He has worked on several projects that turn the theory lens to problems in software verification including visibly pushdown languages, ICE-learning for learning inductive invariants, and natural proofs for proving programs that manipulate data structures. His current interests are in software verification, program synthesis, and trustworthy AI.