Description
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.
Program
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.
Publication
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
Program
Keynote speakers
 Andrew Appel, Princeton University |
 Ian Stark, University of Edinburgh |
Invited speakers include
Program committee
 Adriana Compagnoni (Chair), Stevens |
 Amy Felty, University of Ottawa |