iPRA 2022 – the 4th Workshop on Interpolation:
From Proofs to Applications

About the Workshop

iPRA 2022 – the 4th Workshop on Interpolation: From Proofs to Applications is a FLoC 2022 workshop, affiliated with IJCAR 2022. It continues the iPRA workshop series: iPRA 2013 in Saint Petersburg | iPRA 2014 in Vienna | iPRA 2015 in San Francisco.

Starting out from Craig's interpolation theorem for first-order logic, the existence and computation of interpolant formulas became an active research area, with applications in different fields, notably in verification, databases and knowledge representation. There are challenging theoretical and practical questions, for model theoretic as well as proof theoretic approaches. The workshop aims at bringing together researchers working on interpolation and its various applications, based on different approaches, increasing the awareness of the automated reasoning community for challenging open problems related to interpolation.

The workshop will include invited talks, invited tutorials, and contributed talks. Relevant topics include, but are not limited to:

• Applications of interpolation
• Complexity results and limitations
• Definability and interpolation
• Generalizations of Craig interpolation
• Inductive proofs
• Interpolating decision procedures
• Interpolation-based invariant generation
• Interpolation procedures and algorithms
• Logical abduction
• Practical methods for interpolation
• Program analysis and verification
• Proof systems and calculi for interpolation
• Proof transformation techniques
• Relating model theoretic and proof theoretic approaches
• Separability
• Uniform interpolation

Invited Talks

• Bahareh Afshari, University of Gothenburg, Sweden, and University of Amsterdam, The Netherlands Interpolation and Completeness in the Modal Mu-Calculus
  From a proof-theoretic perspective, the idea that interpolation is tied to provability is a natural one. Thinking about Craig interpolation, if a ‘nice’ proof of a valid implication ϕ→ψ is available, one may succeed in defining an interpolant by induction on the proof-tree, starting from leaves and proceeding to the implication at the root. This method has recently been applied even to fixed point logics admitting cyclic proofs. In contrast, for uniform interpolation, there is no single proof to work from but a collection of proofs to accommodate: a witness to each valid implication ϕ→ψ where the vocabulary of ψ is constrained. Working over a set of prospective proofs and relying on the structural properties of sequent calculus is the essence of Pitts' seminal result on uniform interpolation for intuitionistic logic.

  In this talk we will look at how Pitts' technique can be adapted to derive uniform interpolation for the propositional modal μ-calculus. For this we introduce the notion of an interpolation template, a finite (cyclic) derivation tree in a sequent calculus based on the Jungteerapanich-Stirling annotated proof system. Uniform interpolants arise from encoding the structure of interpolation templates within the syntax of the μ-calculus. We will conclude with a somewhat surprising corollary of the interpolation method via cyclic proofs: a straightforward proof of completeness for Kozen's finitary axiomatisation of the μ-calculus.

• Alessandro Gianola, Free University of Bozen-Bolzano, Italy Uniform Interpolants and Model Completions in Formal Verification of Infinite-State Systems [Slides]
  In the last two decades, Craig interpolation has emerged as an essential tool in formal verification, where first-order theories are used to express constraints on the system, such as on the datatypes manipulated by programs. Interpolants for such theories are largely exploited as an efficient method to approximate the reachable states of the system and for invariant synthesis. In this talk, we report recent results on a stronger form of interpolation, called uniform interpolation, and its connection with the notion of model completion from model-theoretic algebra. In addition, we discuss how uniform interpolants can be used in the context of formal verification of infinite-state systems to develop effective techniques for computing the reachable states in an exact way. Finally, we present some results about the transfer of uniform interpolants to theory combinations. We argue that methods based on uniform interpolation are particularly effective and computationally efficient when applied to safety verification of the so-called data-aware processes: these are systems where the control flow of a (business) process can interact with a data storage.
• H. Jerome Keisler, University of Wisconsin, and Jeffrey M. Keisler, University of Massachusetts Boston, Unites States Application of Interpolation in Networks [Slides]
  Abstract: This lecture is about networks consisting of a directed graph in which each vertex is equipped with a language with the Craig interpolation property, along with a knowledge base (set of sentences) in that language. The knowledge bases grow over time according to some set of rules including the following: For any edge between two vertices, any sentence in the first knowledge base that is in the common language can be added to the second knowledge base (intuitively, the first vertex sends a message to the second). We survey a variety of results and problems that arise in this framework. A central question is: Under which conditions will a sentence be eventually provable from the knowledge base at a given vertex.
• Ken McMillan, The University of Texas at Austin, United States Interpolants and Transformational Proof Systems
  Proof-based interpolation can be thought of as a proof transformation that localizes a proof by introducing a cut or lemma. The hope is that such a lemma will be generally useful, for example in synthesizing an inductive proof. Usually, we think of interpolants as a service provided by an automated prover to some higher-level reasoner such as a program verifier. In this talk, however, we will consider interpolation as a proof transformation to be applied during proof search. To motivate this idea, we will first consider CDCL as a transformational proof system, with conflict clauses generated by an interpolating transformation rule. Then we move from ground to quantified clauses. By adding one proof search rule and one interpolating transformation rule, we obtain a stratified CHC solver. Another transformation allows us to obtain more general conflict clauses using interpolation. The proof transformation view allows us to tightly integrate higher-level proof strategies with CDCL. This presents engineering challenges, but has the potential to produce a class of efficient solvers that can exploit the structure of problem instances.

Call for Contributions

For the contributed talks, we solicit submissions in the form of abstracts. The authors of accepted abstracts are required to present their work at the workshop. A book of abstracts will be published online in advance of the event.

We encourage submissions presenting work in progress, tools under development, as well as research of PhD students, such that the workshop can become a forum for active dialog. Presentations of recently published papers are also allowed and encouraged, but please indicate on your submission where the paper was published/presented.

Abstracts (at most one page, excluding references) or extended abstracts (at most 5 pages, excluding references) have to be submitted by the submission deadline. Submissions should be written in English, and preferably formatted in the style of the Springer Publications format for Lecture Notes in Computer Science (LNCS).

Papers should be submitted electronically via EasyChair at

• https://easychair.org/conferences/?conf=ipra2022

The complete call for contributions in text format suitable for posting is available from here.

Book of Abstracts

iPRA 2022 – Book of Abstracts (PDF)

Registration

FloC 2022 will be a physical conference.

Participants of iPRA 2022 have to register with FloC for the workshop day, 11 August 2022.

Important Dates

Program

Schedule and Abstracts in the FLoC Detailed Program

Invited Talks

• Bahareh Afshari Interpolation and Completeness in the Modal Mu-Calculus
• Alessandro Gianola Uniform Interpolants and Model Completions in Formal Verification of Infinite-State Systems [Slides]
• H. Jerome Keisler and Jeffrey M. Keisler Application of Interpolation in Networks [Slides]
• Ken McMillan Interpolants and Transformational Proof Systems

Contributed Talks

• Matthias Baaz and Anela Lolic First-Order Interpolation Derived from Propositional Interpolation
• Dirk Beyer, Nian-Ze Lee and Philipp Wendler Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
• Wesley Fussner and George Metcalfe Interpolation via Finitely Subdirectly Irreducible Algebras
• Andrzej Indrzejczak and Michal Zawidzki When iota Meets lambda
• Adrian Rebola Pardo Interpolants and Interference

Program Committee

Organizers

Contact: ipra2022@easychair.org