From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p0E2EVXk004456 for ; Fri, 14 Jan 2011 03:14:31 +0100 X-IronPort-AV: E=Sophos;i="4.60,320,1291590000"; d="scan'208";a="86736747" Received: from tu140032.ip.tsinghua.edu.cn (HELO [192.168.1.102]) ([166.111.140.32]) by mail2-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-CAMELLIA256-SHA; 14 Jan 2011 03:14:25 +0100 Message-ID: <4D2FB192.50300@inria.fr> Date: Fri, 14 Jan 2011 10:14:42 +0800 From: Frederic Blanqui User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.13) Gecko/20101208 Thunderbird/3.1.7 MIME-Version: 1.0 To: caml-list@inria.fr Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Subject: [Caml-list] New conference - Certified Programs and Proofs Dear colleagues, Certified Programs and Proofs (CPP) is a new international conference dedicated to the development of certified software and proofs. The conference is intended to be a forum for both theorists and practitioners to exchange ideas about certification used in computer science, mathematics, and education. Please read the manifesto (followed by CFP) for our visions. For more information, please go to the CPP web site at http://formes.asia/cpp/. Best regards, Bow-Yaw Academia Sinica, INRIA, and Tsinghua University *********************************************************************** CPP Manifesto In this manifesto, we advocate for the creation of a new international conference in the area of formal methods and programming languages, named Certified Programs and Proofs (CPP). Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. CPP would target any research promoting formal development of certified software and proofs, that is: - the development of certified or certifying programs; - the development of certified mathematical theories; - the development of new languages and tools for certified programming; - new program logics, type systems, and semantics for certified code; - new automated or interactive tools and provers for certification; - results assessed by an original open source formal development; - original teaching material based on a proof assistant. Software today is still developed without precise specification. A developer often starts the programming task with a rather informal specification. After careful engineering, the developer delivers a program that may not fully satisfy the specification. Extensive testing and debugging may shrink the gap between the two, but there is no assurance that the program accurately follows the specification. Such inaccuracy may not always be significant, but when a developer links a large number of such modules together, these ``noises'' may multiply, leading to a system that nobody can understand and manage. System software built this way often contains hard-to-find ``zero-day vulnerabilities'' that become easy targets for the Stuxnet-like attacks. CPP aims to promote the development of new languages and tools for building certified programs and for making programming precise. Certified software consists of an executable program plus a formal proof that the software is free of bugs with respect to a particular dependability claim. With certified software, the dependability of a software system is measured by the actual formal claim that it is able to certify. Because the claim comes with a mechanized proof, the dependability can be checked independently and automatically in an extremely reliable way. The formal dependability claim can range from making almost no guarantee, to simple type safety property, or all the way to deep liveness, security, and correctness properties. It provides a great metric for comparing different techniques and building steady progress in constructing dependable software. The conventional wisdom is that certified software will never be practical because any real software must also rely on the underlying runtime system which is too low-level and complex to be verifiable. In recent years, however, there have been many advances in the theory and engineering of mechanized proof systems applied to verification of low-level code, including proof-carrying code, certified assembly programming, local reasoning and separation logic, certified linking of heterogeneous components, certified protocols, certified garbage collectors, certified or certifying compilation, and certified OS-kernels. CPP intends to be a driving force that would facilitate the rapid development of this exciting new area, and be a natural international forum for such work. The recent development in several areas of modern mathematics requires mathematical proofs containing enormous computation that cannot be verified by mathematicians in a whole lifetime. Such development has puzzled the mathematical community and prompted some of our colleagues in mathematics and computer science to start developing a new paradigm, formal mathematics, which requires proofs to be verified by a reliable theorem prover. As particular examples, such an effort has been done for the four-color theorem and has started for the sphere packing problem and the classification of finite groups. We believe that this emerging paradigm is the beginning of a new era. No essential existing theorem in computer science has been considered yet worth a similar effort, but it could well happen in the very near future. For example, existing results in security would often benefit from a formal development allowing to exhibit the essential hypotheses under which the result really holds. CPP would again be a natural international forum for this kind of work, either in mathematics or in computer science, and participate strongly to the emergence of this paradigm. On the other hand, there is a recent trend in computer science to formally prove new results in highly technical subjects such as computational logic, at least in part. In whichever scientific area, formal proofs have three major advantages: no assumption can be missing, as is sometimes the case; the result cannot be disputed by a wrong counterexample, as it sometimes happens; and more importantly, a formal development often results in a better understanding of the proof or program, and hence results in easier and better implementation. This new trend is becoming strong in computer science work, but is not recognized yet as it should be by traditional conferences. CPP would be a natural forum promoting this trend. There are not many proof assistants around. There should be more, because progress benefits from competition. On the other hand, there is much theoretical work that could be implemented in the form of a proof assistant, but this does not really happen. One reason is that it is hard to publish a development work, especially when this requires a long term effort as is the case for a proof assistant. It is even harder to publish work about libraries which, we know all, are fundamental to make the success of a proof assistant. CPP would take a particular attention in publishing, publicizing, and promoting this kind of work. Finally, CPP also aims to be a publication arena for innovative teaching experiences, in computer science or mathematics, using proof assistants in an essential way. These experiences could be submitted in an innovative format to be defined. CPP would be an international conference initially based in Asia. Formal methods in Asia based on model checking have been boosted by ATVA. An Asian community in formal methods based on formal proofs is now emerging, in China, South Korea, Taiwan, and Japan (where the use of such formal methods is recent despite a strong logical tradition), but is still very scattered and lacks a forum where researchers can easily meet on a regular basis. CPP is intended to nurse such a forum, and help boosting this community in Asia as ATVA did for the model checking community. For its start, CPP will join APLAS, to be organized in early December 2011 in Taiwan. Co-locating with APLAS will have the advantage of having a larger community present for the very first CPP meeting. In the long run, we would target a three-year rotating schema among Asia, Europe, and North America, and favor colocations with other conferences on each continent. by Jean-Pierre Jouannaud and Zhong Shao December 15, 2010 *********************************************************************** The First International Conference on Certified Programs and Proofs (CPP 2011) PRELIMINARY CALL FOR PAPERS Taiwan December 7--9, 2011 http://formes.asia/cpp (co-located with APLAS 2011) CPP is a new international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates. We invite submissions on topics that fit under this rubric. Suggested, but not exclusive, specific topics of interest for submissions include: certified or certifying programming, compilation, linking, OS kernels, runtime systems, and security monitors; program logics, type systems, and semantics for certified code; certified decision procedures, mathematical libraries, and mathematical theorems; proof assistants and proof theory; new languages and tools for certified programming; program analysis, program verification, and proof-carrying code; certified secure protocols and transactions; certificates for decision procedures, including linear algebra, polynomial systems, SAT, SMT, and unification in algebras of interest; certificates for semi-decision procedures, including equality, first-order logic, and higher-order unification; certificates for program termination; logics for certifying concurrent and distributed programs; higher-order logics, logical systems, separation logics, and logics for security; and teaching mathematics and computer science with proof assistants. IMPORTANT DATES: Authors are required to submit a paper title and a short abstract before submitting the full paper. The submission should include when necessary a url where to find the formal development assessing the essential aspects of the work. All submissions will be electronic. All deadlines are at midnight (GMT). Abstract Deadline: Monday, June 13, 2011 Paper Submission Deadline: Friday, June 17, 2011 Author Notification: Monday, August 29, 2011 Camera Ready: Monday, September 19, 2011 Conference: December 7-9, 2011 SUBMISSION INSTRUCTIONS: Papers should be submitted electronically online via the conference submission web page at URL: http://www.easychair.org/conferences/?conf=cpp2011 Acceptable formats are PostScript or PDF, viewable by Ghostview or Acrobat Reader. Submissions should not exceed 16 pages in LNCS format, including bibliography and figures. Submitted papers will be judged on the basis of significance, relevance, correctness, originality, and clarity. They should clearly identify what has been accomplished and why it is significant. The proceedings of the symposium is planned to be published as a volume in Springer-Verlag's Lecture Notes in Computer Science series. Submission instructions including Latex style files are available from the CPP 2011 website. Each submission must be written in English and provide sufficient detail to allow the program committee to assess the merits of the paper. It should begin with a succinct statement of the issues, a summary of the main results, and a brief explanation of their significance and relevance to the conference, all phrased for the non-specialist. Technical and formal developments directed to the specialist should follow. Whenever appropriate, the submission should come along with a formal development, using whatever prover, e.g., Agda, Coq, Elf, HOL, HOL-Light, Isabelle, Matita, Mizar, NQTHM, PVS, Vampire, etc. References and comparisons with related work should be included. Papers not conforming to the above requirements concerning format and length may be rejected without further consideration. The results must be unpublished and not submitted for publication elsewhere, including the proceedings of other published conferences or workshops. The PC chairs should be informed of closely related work submitted to a conference or journal in advance of submission. Original formal proofs of known results in mathematics or computer science are among the targets. One author of each accepted paper is expected to present it at the conference. AWARD FOR BEST PAPER: An award will be given for the best accepted paper, as judged by the program committee. Details concerning eligibility criteria and procedure for consideration for this award will be posted at the CPP website. The committee may decline to make the award or split it among several papers. PROGRAM CO-CHAIRS: Jean-Pierre Jouannaud (INRIA and Tsinghua University) Zhong Shao (Yale University) Email: cpp2011pc@gmail.com GENERAL CHAIR: Yih-Kuen Tsay (National Taiwan University) PROGRAM COMMITTEE: Andrea Asperti (University of Bologna) Gilles Barthe (IMDEA Software Institute) Xiao-Shan Gao (Chinese Academy of Sciences) Georges Gonthier (Microsoft Research Cambridge) Chris Hawblitzel (Microsoft Research Redmond) John Harrison (Intel Corporation) Jean-Pierre Jouannaud (INRIA and Tsinghua University) Akash Lal (Microsoft Research India) Xavier Leroy (INRIA Paris-Rocquencourt) Yasuhiko Minamide (University of Tsukuba) Shin-Cheng Mu (Academia Sinica) Michael Norrish (NICTA) Brigitte Pientka (McGill University) Sandip Ray (University of Texas at Austin) Natarajan Shankar (SRI International) Zhong Shao (Yale University) Christian Urban (TU Munich) Viktor Vafeiadis (Max Planck Institute for Software Systems) Stephanie Weirich (University of Pennsylvania) Kwangkeun Yi (Seoul National University) PUBLICITY CHAIR: Bow-Yaw Wang (Academia Sinica, INRIA and Tsinhua University) ORGANIZING COMMITTEE: Tyng-Ruey Chuang (chair), Shin-Cheng Mu, Yih-Kuen Tsay (Academia Sinica and National Taiwan University) Email: cpp2011oc@gmail.com