From Concept Learning to SAT-Based Invariant Inference (Invited Talk)

Author Sharon Shoham

Thumbnail PDF


  • Filesize: 319 kB
  • 1 pages

Document Identifiers

Author Details

Sharon Shoham
  • Tel Aviv University, Israel

Cite AsGet BibTex

Sharon Shoham. From Concept Learning to SAT-Based Invariant Inference (Invited Talk). In 43rd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 284, p. 4:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Theory and algorithms for application domains
  • Theory of computation → Program verification
  • Software and its engineering → Formal methods
  • invariant inference
  • complexity
  • exact learning
  • interpolation
  • IC3


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads