From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 87C067F89E for ; Mon, 31 Mar 2014 18:49:38 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of geoff@cs.miami.edu) identity=pra; client-ip=192.31.89.6; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="geoff@cs.miami.edu"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of geoff@cs.miami.edu designates 192.31.89.6 as permitted sender) identity=mailfrom; client-ip=192.31.89.6; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="geoff@cs.miami.edu"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mcclellan.cs.miami.edu) identity=helo; client-ip=192.31.89.6; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="geoff@cs.miami.edu"; x-sender="postmaster@mcclellan.cs.miami.edu"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqsBAJKbOVPAH1kGl2dsb2JhbABZg0GNc584AY8OiGsOAQEBAQEIFgc8gkkhKkANMAQdTQuHZQ2fE6sEhgQXjFiBT4MND2eBFASUYoNrgTSLO4kTIYEs X-IPAS-Result: AqsBAJKbOVPAH1kGl2dsb2JhbABZg0GNc584AY8OiGsOAQEBAQEIFgc8gkkhKkANMAQdTQuHZQ2fE6sEhgQXjFiBT4MND2eBFASUYoNrgTSLO4kTIYEs X-IronPort-AV: E=Sophos;i="4.97,766,1389740400"; d="scan'208";a="65638534" Received: from mcclellan.cs.miami.edu ([192.31.89.6]) by mail2-smtp-roc.national.inria.fr with SMTP; 31 Mar 2014 18:49:37 +0200 Received: by mcclellan.cs.miami.edu (Postfix, from userid 501) id A5169121479; Mon, 31 Mar 2014 12:49:33 -0400 (EDT) To: caml-list@inria.fr Message-Id: <20140331164933.A5169121479@mcclellan.cs.miami.edu> Date: Mon, 31 Mar 2014 12:49:33 -0400 (EDT) From: geoff@cs.miami.edu (Geoff Sutcliffe) X-Validation-by: geoff@cs.miami.edu Subject: [Caml-list] FLoC workshops - Interpolation, Vampire ------------------------------------------------------------------------------ iPrA 2014 - 2ND WORKSHOP ON INTERPOLATION: FROM PROOFS TO APPLICATIONS CALL FOR CONTRIBUTIONS Date: July 17-18, 2014 Location: Vienna, Austria (co-located with the Vienna Summer of Logic) Web: http://vsl2014.at/meetings/iPRA-index.html IMPORTANT DATES Submission deadline: April 30, 2014, AOE Notification: May 7, 2014 Workshop: July 17-18, 2014 ORGANISATION AND COMMITTEE Laura Kovacs and Georg Weissenbacher SCOPE 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 ... FORMAT 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. INVITED TALKS 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. SUBMISSION INSTRUCTIONS Abstracts (at most one page in PDF format) have to be submitted until April 30 via the EasyChair system: https://www.easychair.org/conferences/?conf=ipra2014 The authors will be notified on May 7, 2014. There will be no formal workshop proceedings. REGISTRATION Registration for the workshop will be possible via the VSL registration site http://vsl2014.at/registration/. ------------------------------------------------------------------------------ ========================= Vampire 2014: The Vampire Workshop July 23, 2014, part of FLoC 2014 Vienna, Austria http://www.easychair.org/smart-program/VSL2014//Vampire-index.html ========================= CALL FOR PAPERS ========================= IMPORTANT DATES: Submission deadline:deadlineMay 12, 2014 Notification of acceptance: May 19, 2014 Final paper submission: May 23, 2014 Workshop day:dayJuly 23, 2014 WORKSHOP AIM: The workshop aims at discussing the development and use of the first-order theorem prover Vampire. The workshop will address the newest trends in implementing first-order theorem provers, and focus on new challenges and application areas. Workshop participants will include both Vampire developers and users and provides a convenient opportunity for interesting discussions between tool developers and users. The users can learn more about Vampire and its recent developments. The developers can learn more about the use of Vampire, its efficiency in various application areas and needs of the users. The workshop is going to to shed the light on on problems such as - what is essential for substantial progress in theorem proving tools; - what are the best implementation principles to be used; - what are the best heuristics and strategies, depending on application areas; - both successful and unsuccessful case studies; - missing features in modern theorem provers. The workshop will also overview the most recent advances made in Vampire. PAPER SUBMISSION: We seek submissions reporting on theory, application, case studies, experiments and work-in-progress using Vampire and other theorem provers in various applications. Submissions can be in any form, ranging from work in progress to completed work. For example, the users can submit: - extended abstracts or full papers; - theoretical papers; - experimental papers and case studies - or in general any papers that can benefit tool developers and users. Papers can be of any length, ranging from 2-page abstracts to full papers up to 20 pages in length. The papers should use the EasyChair LaTeX, Microsoft Word, or ODT templates, which can be found at ... http://www.easychair.org/publications/epic-templates. Submissions should be made using EasyChair, via the link ... https://www.easychair.org/conferences/?conf=vampire2014 The workshop proceedings will be published in the EasyChair EPiC series. PROGRAM COMMITEE: Laura Kovacs (Chalmers University of Technology) - chair Andrei Voronkov (University of Manchester) - chair ------------------------------------------------------------------------------