Download to run: precompiled binaries

1. Download pivc.tar.gz.
2. tar xzf pivc.tar.gz. The root directory of πVC is pivc.
3. cd pivc. Run ./configure, which generates a script pivc/bin/piVC to run πVC.
4. Download the Yices SMT solver. Copy the yices binary into pivc/bin/Linux or pivc/bin/Darwin, depending on your platform.
5. Run pivc/bin/piVC. (From pivc, type ./bin/piVC &.)
6. Optional: If you are an instructor installing πVC on a cluster for students and would like to have students email solutions directly to you from πVC, edit the $email variable of pivc/bin/piVC to point to your email address. After proving a program correct, a student will be asked via a prompt if she would like to have the valid program sent to you. Requires sendmail.

• Check your platform. Is it Linux 2.6/i686 or Mac OS X (10.4, PowerPC)?
• Is the user interface not working? Perhaps you need to edit the $java variable of pivc/bin/piVC to point to your preferred JVM.
• Did you copy the pivc directory to another location after running configure? Rerun ./pivc/configure to generate a new execution script.

Download to hack: source code

1. Verify that your system has ocamlc, ocamlopt, and javac.
2. Download pivc-source.tar.gz.
3. tar xzf pivc-source.tar.gz. The root directory of the πVC source code is pivc.
4. Modify the variables OCAML and JAVA of Makefile and Makefile.opt to reflect your system. OCAML should point to the directory that contains O'Caml's libraries. JAVA should point to the directory that contains javac.
5. Type make for bytecode and make -f Makefile.opt for a native binary. (The O'Caml executable is pvc; the GUI is in the jar-file gui/Pi.)
6. Type make install to create the pivc directory hierarchy with root pivc.
7. Copy the pivc directory structure to the desired location.
8. cd pivc. Run ./configure, which generates a script pivc/bin/piVC to run πVC.
9. Download the Yices SMT solver. Copy the yices binary into pivc/bin/Linux or pivc/bin/Darwin, depending on your platform.
10. Run pivc/bin/piVC. (From pivc, type ./bin/piVC &.)

Development of πVC was supported by the National Science Foundation under Grant Nos. CSR-0615449 and CNS-0411363, by Navy/ONR contract N00014-03-1-0939, and by a Sang Samuel Wang Stanford Graduate Fellowship. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation or the Navy/ONR.