Touchstone and Proof-Carrying Code Demo

This interface allows you to try out our Java certifying compiler for x86. The input of the compiler can be either Java source or a set of Java class files (bytecode). The result of the compilation is an x86 assembly language file along with some loop invariant annotations. These annotations are then examined by a simple theorem prover that produces a proof that the x86 assembly language is just as type safe as the corresponding Java bytecode would be. This ultimate effect is that you get the safety of bytecode with the performance of  machine code, without having to trust a complex just-in-time compiler.  

Note: This is work on progress. While the PCC infrastructure is very stable and the Touchstone compiler seems reliable, the Perl cgi-scripts that comprise this Web interface have not been tested extensively. Please be patient, if you run into problems.

Step 1. Read about Touchstone and Proof-Carrying Code.

Step 2.

Select one of our test sources,
Or, select -upload file- above and upload your own sources. Here are a few syntactic constraints that your source must satisfy. (not yet available)

Step 3. Select a suitable set of compiler and prover options. We will add more configuration options in the future.

Optimize proofs (use oracles)

Step 4.

Author: George Necula (necula@cs.berkeley.edu)

Last updated: 02/21/01 10:43:45 AM.