README for the complete piVC distribution (piVC main server, decision procedure server and client)

About this Distribution

This distribution provides everything needed to use piVC. There are 3 components to the piVC system.

1. Client: This is a light-weight Java application that allows users to edit files and send them to the main server for compilation. Note that the client does not do any compilation itself.
2. Main server: This server compiles the programs, produces the verification conditions (VCs), and queries the DP server to determine whether the VCs are valid. It then returns this information to the client.
3. DP server: This server receives VCs from the main server, applies a decision procedure to determine their validity, and returns this information to the main server. The DP server is a stand-alone binary so that it may be replaced with other, potentially proprietary decision procedures.

Note that for most users, the distinction between the main server and DP server is not relevant. There is a binary "both_servers" that runs both.

Typical Use-Case of This Distribution

Instructor: Run the piVC server on a powerful computer by executing bin/both_servers (or perhaps use the server that we provide - see the note at the end of this section). Change the submit_to_email_address and server_address variables in the file src/client/java_gui/ENVIRONMENT. Run make from src/client. Distribute bin/PiGui.jar to the class.

Student: Download and run PiGui.jar.

Note: The instructor might not need to run their own server. We host a piVC server at pivc.stanford.edu:4242. However, we cannot guarantee availability of this server. If you want to use it for a class, you should contact us first (jasonaue@cs.stanford.edu and galenson@cs.stanford.edu).

Requirements

Server: *nix system (Linux, Unix, Mac, Cygwin, etc) with OCaml version 3.09 or above. Client: Sun Java 5.0 or above with support for a GUI.

Installation Instructions

1. "make" from the src directory
2. Do one of the following. 2a. Download the Yices 1 binary from http://yices.csl.sri.com/ (under "Previous releases"). Put the binary into the "bin" directory of this piVC distribution. or 2b. If you already have Yices 1 on your computer, edit the "yices_path" variable of conf/pivc-dp-server.conf to point to the location of yices. 2c. There is experimental support for using Z3. To enable it, modify the conf/*.conf files to use Z3 for the solver name and path.

Configuration Instructions

Client: Instructors will probably want to edit the server_address and submit_to_email_address variables in src/client/java_gui/ENVIRONMENT before distributing PiGui to their students. If these variables are not set, PiGui uses a server address of pivc.jasonland.com:4242 by default (but allows users to change it using the GUI) and prompts the user for an instrutor's email address upon submission.

Server: No configuration should be required. That being said, there is a conf directory with all relevent configuration files.

The main use of these configuration files is probably to change the ports. The default ports are 4242 for the main server and 4243 for the DP server. If you want to change these defaults, edit the files conf/pivc-server.conf and conf/pivc-dp-server.conf. If you change the DP server's port, be sure to update both the "dp_server_address" variable in conf/pivc-server.conf AND the "port" variable in conf/pivc-dp-server.conf.

If you want to run the DP server on a separate machine to the main server, then change the "dp_server_address" variable in conf/pivc-server.conf.

Running Instructions

Servers (main server and DP server combined): Run the binary "both_servers" (in the bin directory). If desired, you can also run the main server and DP server separately using the binaries "main_server" and "dp_server". Client: Launch PiGui.jar (in the bin directory). This is a standard Java JAR file. On some operating systems, double-clicking will run the program. If this does not work, the program can be launched by entering the command java -jar PiGui.jar into a terminal.