Stevens professor to chair International Workshop on PCC

Workshop will bring together those adapting PCC in academia and industry

Adriana Compagnoni, an Associate Professor in the Department of Computer Science at Stevens Institute of Technology, will chair the International Workshop on Proof-Carrying Code in Seattle, August 11, 2006. The workshop aims to bring together people from academia and industry and promote the collaboration between those adapting Proof-Carrying Code (PCC) ideas to new industrial applications and experts in logic, type theory, programming languages, static analysis and compilers.

The meeting, affiliated with IEEE Symposium on Logic in Computer Science (LICS 2006) and part of the Federated Logic Conference (FLoC 2006), will have two keynote speakers, Andrew Appel, Professor of Computer Science at Princeton University, and Ian Stark, Lecturer in Computer Science at University of Edinburgh, representing ongoing research in Europe and the US. The workshop will also feature presentations by invited speakers from academia and industry. Invited speakers include Amal Ahmed, a postdoctoral fellow at Harvard University; Gilles Barthe, researcher and head of the EVEREST team at INRIA Sophia-Antipolis; Ricardo Medel, a Ph.D. candidate in Stevens' Department of Computer Science; Zhong Shao, Professor of Computer Science at Yale University; and Dachuan Yu, a research engineer at DoCoMo Labs.

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, the workshop particularly encourages submissions by students.

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.


About Stevens Institute of Technology
Established in 1870, Stevens offers baccalaureate, masters and doctoral degrees in engineering, science, computer science, management and technology management, as well as a baccalaureate in the humanities and liberal arts, and in business and technology. Located directly across the Hudson River from Manhattan, the university has enrollments of approximately 1,780 undergraduates and 2,700 graduate students, and a current enrollment of 2,250 online-learning students worldwide. Additional information may be obtained from its web page at

For the latest news about Stevens, please visit

Last reviewed: By John M. Grohol, Psy.D. on 21 Feb 2009
    Published on All rights reserved.



Only I can change my life. No one can do it for me.
-- Carol Burnett