Proceedings of the Third International Workshop on Proof-Carrying Code and Software CertificationThis NASA conference publication contains the proceedings of the Third International Workshop on Proof-Carrying Code and Software Certification, held as part of LICS in Los Angeles, CA, USA, on August 15, 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, Vvilich 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 behavior; especially where source code is not available, or the code author and user are unknown to each other. The workshop wiII 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 fonnal 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 featured two invited talks, by Kelly Hayhurst and Andrew Appel. The PCC 2009 website can be found at http://ti.arc.nasa.gov /event/pcc 091.
Document ID
20140000249
Acquisition Source
Ames Research Center
Document Type
Conference Proceedings
Authors
Ewen, Denney, W. (Stinger Ghaffarian Technologies, Inc. (SGT, Inc.) Moffett Field, CA, United States)
Jensen, Thomas (Institut National de Recherche d'Informatique et d'Automatique Le Chesnay, France)
Date Acquired
January 16, 2014
Publication Date
October 1, 2009
Subject Category
Computer Programming And Software
Report/Patent Number
NASA/CP-2009-215403ARC-E-DAA-TN787
Meeting Information
Meeting: International Workshop on Proof-Carrying Code and Software Certification
Location: Los Angeles, CA
Country: United States
Start Date: August 15, 2009
Sponsors: Institute of Electrical and Electronics Engineers
IDRelationTitle20150004723WorkProof Compression and the Mobius PCC Architecture for Embedded Devices20150004716WorkProof-Carrying Code with Correct Compilers20150004718WorkDeriving Safety Cases from Machine-Generated Proofs20150004719WorkPCC Framework for Program-Generators20150004722WorkTowards PCC for Concurrent and Distributed Systems (Work in Progress)20150004720WorkAssurance Cases for Proofs as Evidence20150004715WorkMending the Gap, An Effort to Aid the Transfer of Formal Methods Technology20150004717WorkEfficient Type Representation in TAL20150004721WorkTowards a Certified Lightweight Array Bound Checker for Java Bytecode