CFP: Special Journal Issue on Proof-Carrying Code

[Amy Felty]

Call for Papers

JOURNAL OF AUTOMATED REASONING

Special issue on PROOF-CARRYING CODE

Proof-carrying code is a technology that allows a host, or code
consumer, to safely run code delivered by an untrusted code producer.
The code producer delivers both a program and a formal proof that
verifies that the code meets the desired safety policies.  Safety
policies generally express properties that prohibit the code from
harmful behavior such as accessing private data, overwriting important
data, accessing unauthorized resources, or consuming too many
resources.  Ideally, a proof is constructed automatically, and proof
search may be directed using information that is passed on from the
code producer's compiler.  Proofs provided semi-automatically or
interactively using a proof assistant are possible as well.  Upon
receiving the code and proof, the code consumer uses a mechanical
proof checker to check the proof before executing the code.

This special issue will be devoted to the topic of proof-carrying code
and related approaches which use formal reasoning to enhance safety
and reliability of software.  Manuscripts emphasizing original results
and study of tools and methods for proof generation, proof checking,
and their integration with code generation/compilation are of
particular interest.

Manuscripts should be unpublished works and not submitted elsewhere.
Revised and enhanced versions of papers published in conference
proceedings that have not appeared in archival journals are eligible
for submission.  All submissions will be reviewed according to the
usual standards of scholarship and originality.  Information on JAR
submissions can be found at URL http://www-unix.mcs.anl.gov/JAR/.
Please format your submissions using JAR macros (available at
http://www.wkap.nl/kaphtml.htm/STYLEFILES).

Submissions should be sent to the guest editor in postscript format,
preferably gzipped and uuencoded.  In addition, please send as plain
text, the title, authors, abstract, and contact information for the
paper.  The submission deadline is February 22, 2002.

Guest Editor:
Amy Felty, University of Ottawa, afelty@site.uottawa.ca

This information is available on the web at:
http://www.site.uottawa.ca/~afelty/jar-pcc/