[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: pvs@xxxxxxxxxxx*Subject*: [PVS] PxTP 2012 (IJCAR Workshop) - Call for Papers*From*: Tjark Weber <tjark.weber@xxxxxxxx>*Date*: Sat, 10 Mar 2012 13:42:57 +0100*DKIM-Signature*: v=1; a=rsa-sha256; c=simple/simple; d=uu.se; s=centralsmtp;t=1331383404; i=@uu.se;bh=Ks0dIwEDZh5CYlYVB+Is//BA9AyjDizRhX4HIzlfzCI=;h=Message-ID:Subject:From:To:Content-Type:Date:Mime-Version:Content-Transfer-Encoding;b=s9zHKaRKrP+cNLIIL4GCnYfQt/h3arVZsLLaf/53oJprP3TvKW+PBR2O1t9ZjYf3snSniJWjas/JGd6Tnbm6q/aUsNlO9Y2hudx+JUs6MYGviOxZzXxMc85fKdbnnumbsze03ev8LH+oYN2Vfyh5zB58BPHOKbTFADxCRh+pEOg=*List-Archive*: <http://lists.csl.sri.com/mailman/private/pvs>*List-Help*: <mailto:pvs-request@csl.sri.com?subject=help>*List-Id*: PVS <pvs.csl.sri.com>*List-Post*: <mailto:pvs@csl.sri.com>*List-Subscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs>,<mailto:pvs-request@csl.sri.com?subject=subscribe>*List-Unsubscribe*: <http://lists.csl.sri.com/mailman/listinfo/pvs>,<mailto:pvs-request@csl.sri.com?subject=unsubscribe>*Sender*: pvs-bounces+archive=csl.sri.com@xxxxxxxxxxx

The Second International Workshop on Proof Exchange for Theorem Proving (PxTP) http://pxtp2012.inria.fr associated with The International Joint Conference on Automated Reasoning (IJCAR), 2012 ---------------------------------------------------------------------- The goal of this 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 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). ---------------------------------------------------------------------- Submissions Submitted papers must fall into one of the following two categories: * Short papers: up to 6 pages, work in progress, experience reports, tool presentations or position statements * 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. Short submissions that could stimulate fruitful discussion at the workshop are particularly welcome. Submissions should be in standard-conforming Postscript or PDF. Final versions should be prepared in LaTeX using the easychair.cls class file. To submit a paper, go to the EasyChair PxTP page http://www.easychair.org/conferences/?conf=pxtp2012 and follow the instructions there. PxTP will have no formal proceedings, but we intend to provide electronic proceedings on the CEUR-WS website. ---------------------------------------------------------------------- Important dates Submission of papers: April 2nd, 2012 Notification: May 7th, 2012 Camera-ready versions due: May 21th, 2012 Workshop: June 30th, 2012 ---------------------------------------------------------------------- Program Committee Jasmin Blanchette, Technische Universität München, Germany Pascal Fontaine, University of Nancy, France John Harrison, Intel Corporation, USA Leonardo de Moura, Microsoft Research, USA David Pichardie (co-chair), INRIA Rennes, France Aaron Stump, The University of Iowa, USA Geoff Sutcliffe, University of Miami, USA Laurent Théry, INRIA Sophia-Antipolis, France Allen Van Gelder, University of California at Santa Cruz, USA Tjark Weber (co-chair), Uppsala University, Sweden ----------------------------------------------------------------------

- Prev by Date:
**[PVS] CFP: BOOGIE 2012 - 2nd International Workshop on IntermediateVerification Languages** - Next by Date:
**[PVS] Last mile FUTURE COMPUTING 2012 July 22-27, 2012 - Nice,France** - Prev by thread:
**[PVS] CFP: BOOGIE 2012 - 2nd International Workshop on IntermediateVerification Languages** - Next by thread:
**[PVS] Last mile FUTURE COMPUTING 2012 July 22-27, 2012 - Nice,France** - Index(es):