[TYPES/announce] PCC'09 Call for Participation

[David Pichardie]

      Workshop on Proof-Carrying Code and Software Certification  
(PCC'09)
                      August 15, 2009, Los Angeles, California, USA
                                      Affiliated with LICS'09.
                           http://ti.arc.nasa.gov/event/pcc09/

                           CALL FOR PARTICIPATION

IMPORTANT DATES

Early registration deadline: July 26, 2009
   http://compilers.cs.ucla.edu/lics-sas09/registration/
PCC'09 workshop: August 15, 2009

PROGRAM

Invited talks:
   Kelly Hayhurst, NASA Langley.   Mending the Gap, An effort to aid  
the transfer of formal methods technology

   Andrew Appel, Princeton.    TBA

Workshop talks:
   Juan Chen.   Efficient Type Representation in TAL

   Nurlida Basir, Bernd Fischer and Ewen Denney.   Deriving Safety  
Cases from Machine-Generated Proofs

   Soonho Kong, Wontae Choi and Kwangkeun Yi.   PCC Framework for  
Program Generators

   Sagar Chaki, Arie Gurfinkel, Kurt Wallnau and Charles Weinstock.    
Assurance Cases for Proofs as Evidence

   David Pichardie.   Towards a Certified Lightweight Array Bound  
Checker for Java Bytecode

   Andrzej Filinski, Anders Starcke Henriksen, Fritz Henglein.    
Towards PCC for Concurrent and Distributed Systems

   Thomas Jensen.   Proof compression and the Mobius PCC architecture  
for embedded devices

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.

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
Germán Puebla, Technical University of Madrid
Ian Stark, University of Edinburgh



-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20090710/930d700a/attachment-0001.htm