International Workshop on Proof-Carrying Code (PCC 2006)

Friday August 11, 2006, Seattle, USA

and part of the Federated Logic Conference (FLoC 2006)


As pioneered by Necula and Lee, Proof-Carrying Code (PCC) is a technique that allows the safe execution of untrusted code. In the PCC framework the code receiver defines a safety policy that guarantees the safe behavior of programs and the code producer creates a proof that its code abides by that safety policy. Safety policies can give end users protection from a wide range of flaws in binary executables, including type errors, memory management errors, violations of resource bounds, access control, and information flow.

PCC relies on the same formal methods as does program verification, but it has the significant advantage that safety properties are much easier to prove than program correctness. The producer's formal proof will not, in general, prove that the code yields a correct or meaningful result, so this technique cannot replace other methods of program assurance, but it guarantees that execution of the code can do no harm. The proofs can be mechanically checked by the host; the producer need not be trusted at all, since a valid proof is incontrovertible evidence of safety.

PCC has sparked interest throughout the world, from academia to industry, and has motivated a large body of research in typed assembly languages, types in compilation, and formal verification of safety properties, stimulating new interest in formal methods and programming languages technology.

The aim of the workshop is to bring together people from academia and industry and to promote the collaboration between those adapting PCC ideas to new industrial applications and experts in logic, type theory, programming languages, static analysis, and compilers.


The meeting will have two keynote speakers representing ongoing research in Europe and the USA, and invited speakers from academia and industry. There will also be an open poster session to offer the possibility to showcase a broader spectrum of research in the area. Although poster submission is open to everybody actively working in areas related to the meeting, we particularly encourage submissions by students.


There will be informal proceedings with extended abstracts of the presentations published as a Stevens Institute of Technology Tech-Report available at the meeting. We invite speakers and registered participants to submit a paper to a post meeting special issue of MSCS.


Important dates

  • Poster Submission: 31 May 2006
  • Notification: 11 June 2006
  • Workshop: 11 August 2006
  • Program

    Keynote speakers

    Andrew Appel,
    Princeton University
    Ian Stark
    Ian Stark,
    University of Edinburgh

    Invited speakers include

  • Amal Ahmed, Harvard
  • Gilles Barthe, INRIA Sophia-Antipolis
  • Ricardo Medel, Stevens
  • Zhong Shao, Yale
  • Dachuan Yu, DoCoMo Labs
  • Program committee

    Adriana Compagnoni
    Adriana Compagnoni (Chair),
    Amy Felty
    Amy Felty,
    University of Ottawa

    Contact information

    Adriana Compagnoni
    Last modified: Sun Apr 2 09:09:14 EDT 2006