VSL 2014: VIENNA SUMMER OF LOGIC 2014
iPRA Home Page

Interpolation: From Proofs to Applications

Important dates

Abstract submission May 12, 2014
Notification May 19, 2014
Workshop Date July 17-18, 2014
Affiliated with CAV and SAT

Overview

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.

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, description logics, …)
  • Forgetting, variable elimination, and uniform interpolation
  • Complexity results and limitations
  • …

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 different applications of interpolation. We particularly encourage contributions from outside the verification community.

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

You may also be interested in the program of the First IPRA Workshop in St. Petersburg

Invited Speakers

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

Accepted Abstracts

This year's program comprised a number of exciting and diverse talks (click on talk title to download slides - available if provided by the speakers):

Generalized Craig Interpolation for Stochastic Satisfiability Modulo Theories Problems Ahmed Mahdi and Martin Fränzle
Automated Debugging Using Error Invariants
 Chanseok Oh, Martin Schäf, Daniel Schwartz-Narbonne and Thomas Wies
Towards Craig Interpolation for String Constraints Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp Ruemmer and Jari Stenman
Application Patterns of Projection/Forgetting Christoph Wernhard
Specification Synthesis via Generalized Abduction
 Aws Albarghouthi, Isil Dillig, Arie Gurfinkel and Marsha Chechik
Tree-based Modular SMT Solving Georg Schadler and Georg Hofferek
Using Interpolation for the Verification of Security Protocols Marco Rocchetto, Luca Viganò and Marco Volpe
On Enumerating Query Plans via Interpolants from Tableau Proofs David Toman and Grant Weddell
Resolution Based Uniform Interpolation for Expressive Description Logics Patrick Koopmann and Renate A. Schmidt
Interpolation from Clausal Proofs Yakir Vizel and Arie Gurfinkel
Interpolation Strategies Kenneth McMillan
Interpolation and Domain Independence applied to Databases Enrico Franconi, Paolo Guagliardo, Volha Kerhet and Nhung Ngo
Interpolants in Two-Player Games Niklas Een, Alexander Legg, Nina Narodytska and Leonid Ryzhyk
Practical CNF Interpolants Via BDDs Alexander Legg, Nina Narodytska and Leonid Ryzhyk

Organization

Program Committee

If you have questions please contact Laura Kovács or Georg Weissenbacher.