from Proofs to Applications
|Date||July 13-14, 2013|
|Location||St Petersburg Russia|
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.
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.
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.
As part of the workshop program we will have invited talks given by the following distinguished speakers:
- Ken McMillan (Microsoft Research)
- Andrei Voronkov (University of Manchester, EasyChair)
- Pavel Hrubeš (University of Washington)
The titles and abstracts of the talks/tutorials will be announced closer to the date.
|Workshop||July 13-14, 2013|
|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.
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.