Interpolation: From Proofs to Applications
iPRA is an annual workshop on Craig interpolation and its applications in computer science. The Third Workshop on Interpolation will take place on July 18, 2015, and will be collocated with CAV 2015 in San Francisco.
Important Dates
| Date | July 18, 2015 |
| Location | San Francisco (collocated with CAV 2015) |
| Submission Deadline | May 7, 2015 |
| Notification | May 14, 2015 |
Topics and Submission
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 the 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.
All submissions have to be handed in via EasyChair. The submission site is closed now, please come back next year 🙂
Program
Invited speaker: Arie Gurfinkel, SEI/CMU
Location: Grand Hyatt, Room: Filmore A
| Saturday, July 18 | ||
|---|---|---|
| 9:00am to 10:00am | ||
| Explaining Concurrency Bugs with Interpolants | Mitra Tabaei Befrouei | |
| Vermeer: A Tool for Explaining Bugs | Daniel Schwartz-Narbonne | |
| 10:00am to 10:30am | Morning break | |
| 10:30am to 12:00pm | ||
| Domain-Specific Guidance for Craig Interpolation | Philipp Rümmer | |
| Flexible Propositional Interpolator | Leonardo Alt, Grigory Fedyukovich, Antti Hyvärinen, Natasha Sharygina | |
| 12:00pm to 1:30pm | Lunch break | |
| 1:30pm to 2:30pm | Invited Talk: Interpolating Property Directed Reachability | Arie Gurfinkel | 2:30pm to 3:00pm | Quantifier-free Interpolation for Arrays | Jürgen Christ, and Jochen Hoenicke |
| 3:00pm to 3:30pm | Afternoon break | |
| 3:30pm to 5:00pm | Fast BMC and Interpolation | Yakir Vizel, Arie Gurfinkel, Sharad Malik |
| Symbolic Polytopes for Quantitative Interpolation and Verification | Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko | |
| Interpolating Interactively | Ken McMillan | |
Organization
Chairs and committee: Laura Kovács and Georg Weissenbacher.
Poster Download
(Designed by May Chan)
Past Events
Previous instances of the workshop:
- Second Workshop on Interpolation, July 17-18, 2104, Vienna, Austria
- First Workshop on Interpolation, July 13-14, 2013, St. Petersburg, Russia
If you have questions please contact Laura Kovács or Georg Weissenbacher.
