Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 PCC 2000
Proof-carrying code is a technology that enables end users to verify
properties of programs obtained from untrusted code producers. It can
give end users protection from a wide range of flaws in binary
executables, including type errors, memory management errors, and
violations of resource bounds, access controls, and other security
policies. The essential idea is that the code producer must
distribute a proof of the desired properties along with the code, and
that the end user must run the proof and code through a mechanical
proof checker before execution. The proof might be constructed
automatically by the code producer's compiler, semi-automatically
using a proof assistant, or even written by hand.
The Workshop on Proof-Carrying Code aimed to foster discussion and
collaboration between implementors of proof-carrying code systems and
researchers in the foundational areas of logic, static analysis,
programming language semantics, compilers, type theory, and theorem
proving. It was held on the afternoon of Wednesday, June 28, and the
morning of Thursday, June 29, 2000 at the University of Santa Barbara,
California, USA, between LICS
2000 (June 26 to June 28) and SAS 2000 (June 29 to
July 1).
The program consisted of tutorials and reports on work in progress
by invited speakers:
Proof-Carrying Code: Design, Implementation and Applications George Necula
(University of California, Berkeley)
Typed Assembly Language: Type Theory for Machine Code Karl Crary
(Carnegie Mellon University)
Open Problems for Certifying Compilers Greg Morrisett
(Cornell University)
Semantic Models of Types and Machine Instructions for
Proof-Carrying Code Amy Felty
(University of Ottawa)
Mutable Fields in a Semantic Model of Types Amal Ahmed
(Princeton University)
Proof-Directed Compilation and De-Compilation Atsushi Ohori
(Japan Advanced Institute for Science and Technology)
Compiling with Dependent Types Hongwei Xi
(University of Cincinnati)