[TYPES/announce] PCC 2005 Submission Deadline Extended to June 9

[Amy Felty]

                   Call for Posters: PCC 2006
           International Workshop on Proof-Carrying Code
                  Seattle, USA, August 11, 2006

Affiliated with LOGIC IN COMPUTER SCIENCE (LICS 2006)
and part of the Federated Logic Conference (FLoC 2006)

IMPORTANT DATES
Poster Submission      9 June 2006  **** NEW ****
Notification           18 June 2006

KEYNOTE SPEAKERS
   Andrew Appel (Princeton University)
   Ian Stark (University of Edinburgh)

INVITED SPEAKERS
   Amal Ahmed (Harvard University)
   Gilles Barthe (INRIA Sophia-Antipolis)
   Ricardo Medel (Stevens Institute of Technology)
   Zhong Shao (Yale University)
   Dachuan Yu (DoCoMo Labs)

WEB SITES:
PCC 2006: http://www.cs.stevens.edu/~abc/PCC-Workshop.html
LICS 2006: http://www.informatik.hu-berlin.de/lics/lics06/
FLoC 2006: http://research.microsoft.com/floc06/

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.

POSTER SUBMISSIONS: Posters provide a forum for presenting work in an
informal and interactive setting. They are ideal for discussing
current work not yet ready for publication, for PhD thesis summaries
and research project overviews. The length of a poster submission is 2
pages in the Springer LNCS format. Accepted posters will be presented
at a poster session during the workshop. An extended abstract (2
pages) of each accepted poster will be published in the informal
proceedings. Posters must be submitted electronically to
pcc2006 at cs.stevens.edu.

PUBLICATION: There will be informal proceedings with extended
abstracts of the presentations and posters 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 Institute of Technology)
Amy Felty (University of Ottawa)

CONTACT: pcc2006 at cs.stevens.edu