NASA Logo, National Aeronautics and Space Administration

+NASA Home

+Ames Home

+Intelligent Systems Division

Proof Carrying Code and Software Certification (PCC 2009)
Intelligent Systems Division Banner

Workshop on Proof-Carrying Code and Software Certification (PCC'09)

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



  • Early registration deadline: July 26, 2009
  • Final version due: July 10, 2009
  • Notification of acceptance: June 30, 2009
  • Papers due: June 8, 2009


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.

Call for Papers


Mending the Gap, An effort to aid the transfer of formal methods technology

Kelly Hayhurst, NASA Langley

Formal methods can be applied to many of the development and verification activities required for civil avionics software. RTCA/DO-178B, Software Considerations in Airborne Systems and Equipment Certification, gives a brief description of using formal methods as an alternate method of compliance with the objectives of that standard.Despite this, the avionics industry at large has been hesitant to adopt formal methods, with few developers have actually used formal methods for certification credit.Why is this so, given the volume of evidence of the benefits of formal methods? This presentation will explore some of the challenges to using formal methods in a certification context and describe the effort by the Formal Methods Subgroup of RTCA SC-205/EUROCAE WG-71 to develop guidance to make the use of formal methods a recognized approach.

Talk to be announced soon.

Andrew Appel (Princeton).


Submitted papers must be formatted in the EasyChair class style. There are two categories of submissions:
  • Regular papers describing fully developed work and complete results (10 pages/ 30 minute talks)
  • Short papers describing interesting work in progress and/or preliminary results (5 pages / 15 minute talks)

All papers should describe original work that has not been published elsewhere. Submissions will be fully reviewed and the symposium proceedings will appear as a NASA Conference Publication. Authors of selected papers will then be invited to submit extended versions to a special issue of the journal Higher Order and Symbolic Computation.

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.

Papers should be submitted through the following link:


Proceedings will be made available in electronic format as a technical report. There will be a follow-up special issue of the Higher Order and Symbolic Computation on the topics of proof-carrying code and software certification (more details will be announced at the workshop).

Program Committee:

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

Related Links:

LICS 2009
PCC 2008
SoftCeMent 2005

Web Administrator:

Allen Dutra, NASA Ames
First Gov logo
NASA Logo -