Overview

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 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 features two keynote speakers representing ongoing research in Europe and the USA, and invited speakers from academia and industry. There is also be an open poster session which showcases a broader spectrum of research in the area.

Program

• PCC program
• PCC pre-proceedings

Keynote Speakers

Andrew Appel, Princeton University

Ian Stark, University of Edinburgh

Invited Speakers

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

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.

Program Committee

Adriana Compagnoni (Chair), Stevens

Amy Felty, University of Ottawa

Contact information