The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

(We apologize if you receive multiple copies of this message)

============================================================

                        CALL FOR PAPERS
                           PCC 2009

                3rd International Workshop on 
        Proof Carrying Code and Software Certification

                      August 15, 2009 
                  Affiliated with LICS'09
               Los Angeles, California, USA

             http://ti.arc.nasa.gov/event/pcc09/

============================================================

IMPORTANT DATES
---------------
Papers due:   May 29, 2009
Notification of acceptance:     June 22, 2009
Final version due:  July 10, 2009


SCOPE
-----
Software certification demonstrates the reliability, safety, or
security of software systems in such a way that it can be checked by
an independent authority with minimal trust in the techniques and
tools used in the certification process itself. It can build on
existing validation and verification (V&V) techniques but introduces
the notion of explicit software certificates, which contain all the
information necessary for an independent assessment of the
demonstrated properties. One such example is proof-carrying code (PCC)
which is an important and distinctive approach to enhancing trust in
programs. It provides a practical framework for independent assurance
of program behaviour; especially where source code is not available,
or the code author and user are unknown to each other.

The workshop will address theoretical foundations of logic-based
software certification as well as practical examples and work on
alternative application domains. Here "certificate" is construed
broadly, to include not just mathematical derivations and proofs but
also safety and assurance cases, or any formal evidence that supports
the semantic analysis of programs: that is, evidence about an
intrinsic property of code and its behaviour that can be independently
checked by any user, intermediary, or third party. These guarantees
mean that software certificates raise trust in the code itself,
distinct from and complementary to any existing trust in the creator
of the code, the process used to produce it, or its distributor.

In addition to the contributed talks, the workshop will feature two
invited talks.


SUBMISSION
----------
Two types of submissions are solicited:
- Standard papers (at most 10 pages) describing novel research results.
- Short papers (at most 5 pages) describing a novel idea that is 
work-in-progress.

Additional material intended for the referees but not for publication
in the final version may be placed in a clearly marked appendix that
is not included in the page limit.

Authors are invited to submit their papers electronically, in PDF
format via the EasyChair submission web page:
http://www.easychair.org/conferences/?conf=pcc09

All submissions will be fully reviewed.


PUBLICATION
-----------
Proceedings will be made available in electronic format as a technical
report. A follow-up special issue of a journal on the topics of
proof-carrying code and software certification is under consideration.


PROGRAM COMMITTEE
-----------------
David Aspinall, University of Edinburgh
Gilles Barthe, IMDEA Software
Ewen Denney, RIACS/NASA Ames, co-chair
Bernd Fischer, University of Southampton
Sofia Guerra, Adelard
Kelly Hayhurst, NASA Langley
Thomas Jensen, IRISA/CNRS, co-chair
David Pichardie, INRIA
German Puebla, Technical University of Madrid
Ian Stark, University of Edinburgh