Background
The goal of this new workshop is to bring together researchers working on proof production from automated theorem provers with potential consumers of proofs. Machine-checkable proofs have been proposed for applications like proof-carrying code and certified compilation, as well as for exchanging knowledge between different automated reasoning systems. For example, interactive theorem provers can import results from otherwise untrusted high-performance solvers, by means of proofs the solvers produce. In such situations, one automated reasoning tool can make use of the results of another, without having to trust that the second tool is sound. It is only necessary to be able to reconstruct a proof that the first tool will accept, in order to import the result without increasing the size of the trusted computing base.
This simple idea of proof exchange for theorem proving becomes quite complicated under the real-world constraints of highly complex and heterogeneous proof producers and proof consumers. For example, even the issue of a standard proof format for a single class of solvers, like SMT solvers, is quite difficult to address, as different solvers use different inference systems. It may be quite challenging, from an engineering and possibly also theoretical point of view, to fit these into a single standard format. Emerging work from several groups proposes standard meta-languages or parametrized formats to achieve flexibility while retaining a universal proof language.
Topics
Topics of interest for this workshop include all aspects of proof exchange among automated reasoning tools. More specifically, some suggested topics are:
- proposed proof formats for different classes of logic solvers (SAT, SMT, QBF, First-Order ATP, Higher-Order ATP, Rewriting, etc.).
- meta-languages and logical frameworks for proofs, particularly proof systems designed for solvers.
- proof checking tools and algorithms.
- proof translation and methods for importing proofs, including proof replaying or reconstruction.
- tools and case studies related to analyzing proofs produced by solvers, and proof metrics.
- applications relying on importing proofs from automated theorem provers, such as certified static analysis, proof-carrying code, or certified compilation.
- data structures and algorithms for improved proof production in solvers (for example, more time- or memory-efficient ways of representing proofs).
Program committee
- Clark Barrett (New York University)
- Christoph Benzmüller (Articulate Software)
- Sacha Böhme (Technische Universität München)
- Amy Felty (University of Ottawa)
- Pascal Fontaine (INRIA, University of Nancy), co-chair
- Leonardo de Moura (Microsoft research)
- Hans de Nivelle (University of Wroclaw)
- David Pichardie (INRIA Rennes)
- Stephan Schulz (Technische Universität München)
- Aaron Stump (The University of Iowa), co-chair
- Geoff Sutcliffe (University of Miami)
- Laurent Théry (INRIA)
- Tjark Weber (University of Cambridge)
- Bruno Woltzenlogel Paleo (Technische Universität Wien)
Submissions
Submitted papers must fall into one of the following two categories
- Short papers: up to 6 pages tool papers or experience reports
- Regular papers: 12-15 pages research papers
Submissions will be refereed by the program committee, which will select a balanced program of high-quality contributions.
Submissions should be in standard-conforming Postscript or PDF.
To submit a paper, go to the EasyChair PxTP page and follow the instructions there.
You can view the full call for papers.
Final versions
Final versions should be prepared in LaTeX using the easychair.cls class file.
Important dates:
- Submission of papers: May 11th, 2011 (Extended)
- Notification: May 30th, 2011
- Camera ready versions due: June 27th, 2011
- Workshop: August 1st, 2011
Proceedings
PxTP will have no formal proceedings, but we anticipate a joint open call, together with the PSATTT workshop (also at CADE 2011), for a special issue of a journal with PxTP and PSATTT post-proceedings.
Download here the full PxTP-2011 proceedings.
Program
| 08:55 - 09:00 | Welcome |
| Session 1: | Chair: Stephan Schulz |
| 09:00 - 10:00 | Jasmin Blanchette Invited Talk: Proof Search and Proof Reconstruction in Sledgehammer Slides Abstract: Sledgehammer is a popular tool included with the Isabelle/HOL interactive theorem prover that discharges interactive goals using resolution provers (E, SPASS, Vampire) and SMT solvers (CVC3, Yices, Z3). The main difficulty with proof search is to encode type information efficiently, including polymorphism. For SMT solvers, we monomorphize the problem and map the resulting ground types to SMT-LIB sorts. For resolution provers, we experimented with a menagerie of type encodings and selected the most appropriate encoding for each prover, sacrificing soundness for efficiency in some cases. For proof reconstruction, several schemes are supported: (1) SMT solvers can be trusted and used as oracles; (2) Z3 proofs are replayed step by step and can be stored as certificates to speed up replay; (3) from resolution proofs, Sledgehammer extracts the used lemmas and attempts to re-find the proofs in Isabelle; (4) experimentally, we also implemented structured Isabelle proof construction from resolution proofs. This last scheme is the most promising, and we are currently working on improving the readability of the proofs and add support for SMT proofs. Joint with PSATTT'11 |
| 10:00 - 10:30 | Coffee |
| Session 2: | Chair: Tjark Weber |
| 10:30 - 11:00 | Frédéric Besson, Pierre-Emmanuel Cornilleau and David Pichardie A Nelson-Oppen based Proof System using Theory Specific Proof Systems Joint with PSATTT'11 |
| 11:00 - 11:30 | Geoff Sutcliffe, Cynthia Chang, Deborah Mcguinness, Tim Lebo, Li Ding and Paulo Pinheiro Da Silva Combining Proofs to form Different Proofs Joint with PSATTT'11 |
| 11:30 - 12:00 | Piotr Rudnicki and Josef Urban Escape to ATP for Mizar |
| 12:00 - 12:30 | Stephan Merz and Hernán Vanzetto Towards certification of TLA+ proof obligations with SMT solvers |
| Session 3: | Chair: Piotr Rudnicki |
| 14.00 - 15.00 | John Harrison Invited Talk: Heterogeneous Theorem Proving, Certification, and Integrated Automation Slides Abstract: Theorem provers are being used for an increasing variety of applications in both formal verification and the formalization of mathematics. However, as these applications grow more complex and diverse, it is increasingly difficult to use a single tool for the entire process. Formal verification activities at Intel use a diverse range of tools and methods: for instance some arithmetic proofs use a combination of symbolic simulation and inductive theorem proving, while some protocol proofs use a combination of model checking and ad-hoc state abstraction programs. A similar situation arises in pure mathematics, with the Flyspeck project to formalize the proof of the Kepler conjecture requiring the formalization of results reached by linear and nonlinear optimization software and ad-hoc graph enumeration software, and with some parts of the formal proof done in different theorem provers. It is thus very desirable to have a principled way of connecting all these tools and methods. Combining them by hand or by ad-oc programs gives rise to two problems: transcription errors at the interfaces between systems, and the increasing difficulty of trusting a large heterogeneous collection of tools. At the very least, one would hope to be able to transfer results in a meaningful way even between systems with different (and perhaps ill-specified) logical foundations. More ambitiously, one would wish to be able to transfer proofs or other "certificates" between such tools, so that logical soundness can be maintained by a complete and rigorous check on all results obtained, perhaps via a general interactive theorem prover that ties all the results together, or a separate and very simple "proof checker". Recent years have seen an increasing number of examples where external tools are used to generate relatively simple certificates that can be checked by other tools. We will survey some interesting examples where this process seems easy and successful and those where it seems difficult, and examine alternative approaches. Finally, even assuming that an interactive theorem prover is equipped with a panoply of classic decision procedures and mathematical solvers, there are still deep challenges in integrating the inferences that these tools can do in isolation, and we will examine some of the challenges and opportunities here. Joint with PSATTT'11 |
| 15.00 - 15.30 | Mickael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller and Laurent Thery Verifying SAT and SMT in Coq for a fully automated decision procedure Joint with PSATTT'11 |
| 15.30 - 16.00 | Coffee |
| Session 4: | Chair: Geoff Sutcliffe |
| 16.00 - 16.30 | Sascha Böhme and Tjark Weber Designing Proof Formats: A User's Perspective |
| 16.30 - 17.00 | Frédéric Besson, Pascal Fontaine and Laurent Théry A Flexible Proof Format for SMT: a Proposal |
| 17:00 - 17:30 | David Deharbe, Pascal Fontaine and Bruno Woltzenlogel Paleo Quantifier Inference Rules for SMT proofs |
| 17:30 - 18:00 | Discussion: Proofs for SMT |
| 19:30 | Informal Workshop Diner Joint with PSATTT'11 |