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.
First, you need to download and unpack the Touchstone sources. These can be found at ftp.cs.cmu.edu. We'll use $ROOT to refer to the top-level Touchstone directory (containing subdirs pcc, cc, and prover).
Set the following environment variables (
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:
ARCHOS, as above.
Main.compileis relative to the
Here's a short description of some of the important directories in this release:
Compiling with Proofs George C. Necula.A few related papers are listed at the Fox Project Publications page.
Maintained by:David.Swasey@cs.cmu.edu (last updated Thu Mar 18 10:13:05 EST 1999 )