PCC 2008 is a joint LICS and CSF affiliated workshop on
Proof-carrying code is an important and distinctive approach to
enhancing trust in programs. It provides a practical framework for
independent assurance of program behaviour; especially where source
code is not available, or the code author and user are unknown to each
The workshop will address theoretical foundations of
proof-carrying code as well as practical examples and work on alternative
application domains. Here "proof" is construed broadly, to
include not just mathematical derivations but any formal evidence that
supports the static 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 manifest guarantees mean
that PCC raises 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.
- PCC addressing properties of safety, security, and correctness such as:
Memory safety, information flow, declassification, resource management,
access control, protocol enforcement, functional correctness.
- Examples of PCC in application domains, including but not limited to:
Mobile code, mobile devices, operating systems, grid computing,
peer-to-peer computing, active networks, embedded systems, cloud
computing, databases, e-Science.
- Probabilistically-checkable proofs, zero-knowledge proofs, proof-on-demand.
- Trust and policy frameworks; supporting modular and extensible systems;
compositionality in code and proofs.
- Certifying compilation, proof-transforming compilation, certified verifiers.
Logics and notions of certificate specific to proof-carrying frameworks.
PCC 2008 follows on from the successful PCC 2006 workshop
Links: Full schedule of talks; Abstracts
Jensen Static Analysis for Extended Byte Code Verification
Shao Modular Development of Certified System Software
- Comparing Semantic and Syntactic Methods in Mechanized Proof
Christian Bell, Robert Dockins, Aquinas Hobor, Andrew W. Appel and David
- Noninterference for Mobile Code with Dynamic Security
- A Logic for
Reasoning About Faulty Programs
Matthew L. Meola, Frances Perry and David Walker.
Limin Jia AURA: A
Programming Language for Authorization and Audit
- Robert Atkey
A Practical PCC Framework for Java Bytecode
- Andrei Sabelfeld
Tight Enforcement of Flexible Information-Release Policies for Dynamic
Registration is being handled centrally by CMU for CSF, LICS, and all
associated workshops. All registrations include lunch, refreshment breaks and
wireless internet access for each day of attendance. You can book dorm
accommodation on campus with conference registration. In addition, LICS and
CSF have also reserved blocks of rooms with local hotels.
- The deadline for early registration is 1 June 2008.
- The deadline for late online registration is 10 June 2008.
- After June 10 you must make special arrangements with the conference
organizers to register on-site.
Links: Online registration, LICS hotels, CSF hotels
- David Aspinall,
University of Edinburgh (co-chair)
Barthe, INRIA Sophia-Antipolis / IMDEA Software, Madrid
- Nick Benton,
Microsoft Research Cambridge
- Adriana Compagnoni, Stevens
Institute of Technology
- Karl Crary, Carnegie Mellon University
- Ewen Denney,
- Hans-Wolfgang Loidl, LMU Munich
- George Necula,
UC Berkeley / Rinera Networks
- Ian Stark, University
of Edinburgh (co-chair)
- Stephanie Weirich,
University of Pennsylvania
|Paper submission: ||2 ||May ||2008
||(Extended by 1 week from original date)|
|Author notification:||23||May ||2008|
|Early registration:||1||June ||2008|
|Final versions: ||7 ||June ||2008|
|Workshop: ||22||June ||2008|
David Aspinall and Ian Stark
Laboratory for Foundations of Computer
School of Informatics
The University of Edinburgh
James Clerk Maxwell Building
The King's Buildings
Edinburgh EH9 3JZ
Contact email: firstname.lastname@example.org
Twenty-Third Annual IEEE Symposium on Logic in Computer Science
CSF: 21st IEEE Computer
Security Foundations Symposium
Mobius: Mobility, Ubiquity,
Enabling proof-carrying code for Java on mobile devices
The University of Edinburgh is a charitable body, registered in Scotland,
with registration number SC005336
Page last modified:
Monday 16 June 2008