Email Gateway (Aug 19 2022 at 10:50): Email Gateway (Aug 19 2022 at 10:50):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Call for Papers, PxTP 2013
EXTENDED DEADLINE
The Third International Workshop on
Proof Exchange for Theorem Proving (PxTP)
(and Cooperation between Theorem Provers)
http://www.cs.ru.nl/pxtp13/
June 10, 2013, Lake Placid, USA
associated with
The Conference on Automated Deduction (CADE), 2013.
Invited Speaker
Thomas C. Hales, University of Pittsburgh, USA
Scope
The PxTP workshop welcomes contributions on various aspects of
communication, integration, and cooperation between reasoning systems
and formalisms.
The past decades have seen impressive advances in computer-aided
reasoning, both in automated and interactive theorem proving. As shown
by various system competitions, such as CASC, SMT-COMP, and the SAT
competition, deduction tools are able to tackle larger problems
progressively faster and are increasingly more applicable to a wider
range of problems. In recent years, integration of such automated
tools in larger verification environments has demonstrated the
potential to reduce the amount of manual verification work.
It is becoming clear that the success of deduction tools will not only
depend on their power to solve large and difficult problems in an
isolated manner, but it will also rely on their ability to cooperate,
by exchanging problems, proofs, and models. The PxTP workshop aims at
encouraging such cooperation by inviting contributions on various
aspects of communication, integration, and cooperation between systems
and formalisms. The workshop's mission is to facilitate building of
complex reasoning applications and reuse of reasoning tools by
developing and discussing suitable integration, translation and
communication methods, standards, protocols, and application
programming interfaces (APIs). We are interested both in success
stories and in descriptions of the current bottlenecks and proposals
for improvement.
Topics of interest for this workshop include all aspects of
cooperation between reasoning tools, whether automatic or interactive.
More specifically, some suggested topics are
-- applications that integrate reasoning tools
(ideally with certification of the result);
-- translations between logics, proof systems, models;
-- distribution of proof obligations among heterogeneous reasoning
tools;
-- algorithms and tools for checking and importing (replaying,
reconstructing) proofs;
-- proposed formats for expressing problems and solutions for
different classes of logic solvers (SAT, SMT, QBF, first-order
logic, higher-order logic, typed logic, rewriting, etc.);
-- meta-languages, logical frameworks, communication methods,
standards, protocols, and APIs connected to problems, proofs, and
models;
-- comparison, refactoring, and optimization of proofs;
-- practical experiences, case studies, feasibility studies;
-- applications relying on importing proofs from automatic theorem
provers, such as certified static analysis, proof-carrying code, or
certified compilation;
-- data structures and algorithms for improved proof production in
solvers (e.g., efficient proof representations).
Submissions
Researchers interested in participating are invited to submit either
an extended abstract (up to 8 pages) or a regular paper (up to 15
pages) via EasyChair.
Submissions will be refereed by the program committee, which will
select a balanced program of high-quality contributions. Short
submissions that could stimulate fruitful discussion at the workshop
are particularly welcome.
Submissions should be in PDF. Final versions should be prepared in
LaTeX using the "easychair.cls" class file, available at
http://www.easychair.org/publications/.
To submit a paper, go to the EasyChair PxTP page
http://www.easychair.org/conferences/?conf=pxtp2013
and follow the instructions there.
PxTP proceedings will be published electronically in the EasyChair
Proceedings in Computing (EPiC) series or in the CEUR workshop
proceedings.
Important dates (updated)
Submission of papers: 22 April 2013 (extended)
Notification: 9 May 2013
Camera-ready versions due: 16 May 2013
Workshop: 10 June 2013
Program Committee
Jasmin Christian Blanchette (co-chair), TU Muenchen, Germany
Chad Brown, Saarland University, Germany
David Delahaye, CEDRIC/CNAM, Paris, France
Ewen Denney, SGT/NASA Ames, USA
Peter Dybjer, Chalmers University, Sweden
Pascal Fontaine, Loria, INRIA, University of Nancy, France
John Harrison, Intel Corporation, USA
Warren Hunt, University of Texas, USA
Chantal Keller, Laboratoire d'Informatique de Polytechnique, France
Konstantin Korovin, Manchester University, UK
Magnus O. Myreen, University of Cambridge, UK
Jens Otten, University of Potsdam, Germany
Andrei Paskevich, Universite Paris-Sud 11, IUT d'Orsay, France
Lawrence C. Paulson, University of Cambridge, UK
David Pichardie, INRIA Rennes - Bretagne Atlantique, France
Florian Rabe, Jacobs University Bremen, Germany
Stephan Schulz, TU Muenchen, Germany
Aaron Stump, CS Department, The University of Iowa, USA
Geoff Sutcliffe, University of Miami, USA
Laurent Thery, INRIA, France
Josef Urban (co-chair), Radboud Universiteit Nijmegen, Netherlands
Tjark Weber, Uppsala University, Sweden
Last updated: Nov 21 2024 at 12:39 UTC