Workshop on Interpolation

from Proofs to Applications

Date July 13-14, 2013
Location St Petersburg Russia

Summary

The first workshop on interpolation was a highly successful event, with 12 speakers and 3 invited talks, more than 40 registered participants and an even larger audience. The quality of the presentations was outstanding, and the slides are available for download below.

Scope

Craig interpolation enjoys a continuing popularity in the field of verification. Historically, Craig’s interpolation theorem has received ample attention in proof theory and mathematical logic as well as in complexity theory. The aim of the workshop is to bring together theoreticians and practitioners from different fields.

The topics of interest comprise but are not limited to:

  • 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, …)
  • Complexity results and limitations
  • …

We particularly encourage contributions from outside the verification community.

Format

The workshop will feature

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

The submission of abstracts describing recently published papers is allowed and encouraged.

Invited Speakers

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

The titles and abstracts of the talks/tutorials will be announced closer to the date.

Program

Saturday, July 13
12.30pm to 2pm Lunch
2pm to 3.30pm Invited Talk: Revisiting Generalizations Ken McMillan
3.30pm to 4pm Coffee break
4p to 6pm Interpolants and SAT-based Model Checking Yakir Vizel
DAG-Interpolation for Software Model Checking Arie Gurfinkel, Aws Albarghouthi
Logical Abduction and Applications in Program Verification Isil and Thomas Dillig
7pm Informal workshop dinner. We made a reservation for 16 people at 7.30pm at the restaurant Gosti, close to Alexander Garden (see information below)
Sunday, July 14
9am to 10.30am Invited Talk: The interpolation technique in proof complexity, and its limitations Pavel Hrubeš
10.30am to 11am Coffee break
11am to 12.30pm Two-stage Interpolation Systems Maria Paola Bonacina
Generating Tiny Interpolants and Near-interpolants from a Resolution Refutation Alexander Nadel, Vadim Ryvchin and Yakir Vizel
PeRIPLO: Proof tRansformer and Interpolator for Propositional LOgic Simone Fulvio Rollini
12.30pm to 2pm Lunch break
2pm to 3.30pm Invited Talk: Interpolation in First-Order Logic and Vampire Andrei Voronkov
3.30pm to 4pm Coffee break
4pm to 6pm Non-linear interpolant generation and its applications to program verification Liyun Dai, Bican Xia and Naijun Zhan
Interpolation goes on SAFARI Francesco Alberti and Simone Fulvio Rollini
Generalised Interpolation by Solving Recursion-Free Horn Clauses Ashutosh Gupta, Corneliu Popeea and Andrey Rybalchenko
6pm to 7pm Discussion on proof formats, proof representations, tooling and benchmarking.

We have allocated 2 hours for each session of 3 contributed talks, leaving plenty of time for discussion. There will be no formal workshop proceedings, but we will distribute the abstracts of the talks on a USB sticks at the workshop.

Informal Workshop Dinner

We made a reservation for 16 people at 7.30pm at the restaurant Gosti, close to Alexander Garden (see map below). It’s a half hour walk, so we will leave at 7pm at the conference hotel. The dinner is not included in the registration. During the workshop, we will pass around a list and ask you to indicate whether you will join or not, so we can update our reservation if necessary.


View Larger Map