Title: SAT-Based Invariant Inference and Its Relation to Concept Learning

Speaker: Sharon Shoham Buchbinder    (bio) (bio)

Sharon Shoham Buchbinder is an Associate Professor in the School of Computer Science at Tel Aviv University. Her main areas of research are formal verification and program analysis.

When: Monday, 17 April 2023 at 1900 hrs (IST)       

Abstract:
In recent years SAT-based invariant inference algorithms such as interpolation-based model checking and PDR/IC3 have proven to be extremely successful in practice. However, the essence of their practical success and their performance guarantees are far less understood. This talk surveys results that establish formal connections and distinctions between SAT-based invariant inference and exact concept learning with queries, showing that learning techniques and algorithms can clarify foundational questions, illuminate existing algorithms, and suggest new directions for efficient invariant inference.