iPRA 2022 – the 4th Workshop on Interpolation:
From Proofs to
Applications
About the Workshop
Invited Talks
Call for Contributions
Book of Abstracts
Registration
Important Dates
Program
Program Committee
Organizers
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 firstorder 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
 Interpolationbased 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

Bahareh
Afshari, University of Gothenburg, Sweden, and University of
Amsterdam, The Netherlands
Interpolation and Completeness in the Modal
MuCalculus
From a prooftheoretic 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 prooftree, 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
JungteerapanichStirling 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 BozenBolzano, Italy
Uniform Interpolants and Model Completions in Formal
Verification of InfiniteState Systems
[Slides]
In the last two decades, Craig interpolation has emerged as an essential
tool in formal verification, where firstorder 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 modeltheoretic
algebra. In addition, we discuss how uniform interpolants can be used in
the context of formal verification of infinitestate 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 socalled
dataaware 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
Proofbased 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 higherlevel 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 higherlevel 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.
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
The complete call for contributions in text format suitable for posting is
available from here.
FloC 2022 will be a physical
conference.
Participants of iPRA 2022 have to
register with FloC for
the workshop day, 11 August 2022.
Invited Talks
Contributed Talks

Matthias Baaz and Anela Lolic
FirstOrder Interpolation Derived from Propositional
Interpolation

Dirk Beyer, NianZe Lee and Philipp Wendler
Interpolation and SATBased 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
Michael
Benedikt 

University of Oxford, UK 
Maria Paola
Bonacina 

Università degli Studi di Verona, Italy 
Silvio
Ghilardi 

Università degli Studi di Milano, Italy 
Arie Gurfinkel 

University of Waterloo, Canada 
Rosalie Iemhoff 

Utrecht University, The Netherlands 
Laura Kovács 

TU Wien, Austria 
Pavel Pudlák 

Czech Academy of Sciences, Czech Republic 
Philipp Rümmer 

Uppsala University, Sweden 
Georg
Weissenbacher 

TU Wien, Austria 
Christoph
Wernhard 

University of Potsdam, Germany 
Frank Wolter 

University of Liverpool, UK 
Organizers
Contact: ipra2022@easychair.org