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