• Date: July 17-18, 2014
  • Location: Vienna, Austria (co-located with the Vienna Summer of Logic)
  • Web:


  • Submission deadline: April 30, 2014, AOE
  • Notification: May 7, 2014
  • Workshop: July 17-18, 2014


Laura Kovacs and Georg Weissenbacher


Craig interpolation enjoys a continuing popularity in computer science. Historically, Craig’s interpolation theorem has received ample attention in proof theory and mathematical logic as well as in complexity theory. Recently, interpolants are increasingly used in automated verification, synthesis, and description logics. The aim of the workshop is to bring together theoreticians and practitioners from these different fields.

We solicit submissions in form of an abstract of at most one page in PDF format. The authors of accepted abstracts are required to present their work at the workshop. There will be no published proceedings.

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 between the groups involved in applications of interpolation. We also encourage contributions from outside the verification community.

Presentations of recently published papers are also allowed and encouraged, but please indicate on your submission where the paper was published/presented.

Relevant topics include (but are not limited to) applications of interpolation in:

  • Interpolating decision procedures
  • Proof theoretic approaches to interpolation
  • Proof systems and calculi for interpolation
  • Proof transformation techniques
  • Inductive Proofs
  • Logical Abduction
  • Interpolation techniques based on constraint solving, linear programming…
  • Alternative techniques for interpolation
  • Interpolation theorems (for theories and extensions, non-classical logic, …)
  • Interpolation-based/Inductive invariant generation
  • Program analysis and verification
  • Tools for interpolation
  • Applications of Craig interpolation (verification, synthesis, automated reasoning, …)
  • Forgetting, variable elimination, and uniform interpolation
  • Complexity results and limitations …


The workshop will feature

  • invited talks and tutorials by distinguished speakers,
  • presentations (selected by a committee based on the submission of abstracts) by workshop participants, and
  • discussion and panel sessions.


As part of the workshop program we will have invited talks given by the following distinguished speakers:

  • Orna Grumberg (Technion, Israel)
  • Pavel Pudlák (Academy of Sciences, Czech Republic)
  • Frank Wolter (University of Liverpool, UK)

The titles and abstracts of the talks/tutorials will be announced on the workshop web-page closer to the date.


Abstracts (at most one page in PDF format) have to be submitted until April 30 via the EasyChair system:

The authors will be notified on May 7, 2014. There will be no formal workshop proceedings.


Registration for the workshop will be possible via the VSL registration site