Proof-Carrying Code

The Touchstone Certifying Compiler

Oct 1998 Release


See also: the Touchstone compiler page, the Proof-Carrying Code page, George Necula's home page, and the Touchstone online demo (more pointers are listed below).


This release of Touchstone works only on Alphas running Digital Unix V3.2 or V4.0. In addition to software that comes with Digital Unix (such as the assembler and linker), you'll need the following: GNU make, gcc, perl5 (installed as /usr/local/bin/perl5), m4, and SML/NJ version 110.

Using Touchstone

First, you need to download and unpack the Touchstone sources. These can be found at We'll use $ROOT to refer to the top-level Touchstone directory (containing subdirs pcc, cc, and prover).

Set the following environment variables (CCOMP and PCC should be absolute paths):

Before you can use Touchstone for the first time, you have to run GNU make in $ROOT/pcc. This builds the programs engine and transl_elf and puts them in $ROOT/pcc/Bin.

Touchstone includes a driver program that knows all the steps necessary to compile a Touchstone C program into proof-carrying code. This driver is the ML function Main.compile. Each time you want to use Touchstone, you need to:

Important Directories

Here's a short description of some of the important directories in this release:

ML source for an optimizing, certifying compiler for a type-safe subset of C
ML source for a theorem prover
C source for:
translates a fully explicit Elf signature into a binary (represented as Alpha assembler input).
Both the VCGen and proof checker for Touchstone. Works with the binary for predicates and proofs, stored in COFF files.
LF logic and axioms for Touchstone's safety policy.
Test code and benchmarks (*.cc) written in Touchstone C. A few of the Touchstone programs include C driver programs (named *.main.c). The Touchstone compiler's log file is stored here (out).
Temporary files and output produced by Main.compile go here.
Contains perl scripts and binaries used during Main.compile.


This work was sponsored in part by the Advanced Research Projects Agency CSTO under the title "The Fox Project: Advanced Languages for Systems Software," ARPA Order No. C533, issued by ESC/ENS under Contract No. F19628-95-C-0050.

Maintained by:
(last updated Thu Mar 18 10:13:05 EST 1999 )