Use Virtualbox to import the downloaded .ova file. After booting the virtual machine, you can log into the machine with
Username: ucsd Password: quark
You can run the verified browser by either (a) clicking the spherical icon on the taskbar to the left, or (b) opening a terminal and running
cd ~/kraken/reflex/coq/bench-quark ./run.sh
More details about the browser are given at
The SSH server is setup to run when the VM is started. Simply login to
localhost to try it out.
More details about the SSH Server are given at
In order to run the web server, do the following:
cd ~/kraken/reflex/coq/bench-webserver/ml ./kernel
Then you can connect to the web server from your favorite web browser and receive some static web pages.
cd ~/kraken/reflex/coq make bench BENCHOUT=<results-dir> TIMEOUT=<timeout>
A single file called
<results-dir>/results.csv will be created, giving, for each property, the time taken to produce a proof (Ltac), the time taken to check the proof (Qed), and the maximum memory used while creating the proof.
You can also tweak the automation optimizations that are run by modifying
Opt.v. This file consists of six boolean valued expressions, each corresponding to an optimization.
Make sure that when you run the automation on these properties, the VM has at least 4GB of memory.
Because of the strange setup in our build system, running the proof automation deletes the binaries for all of our kernels. They must be rebuilt. To rebuild the binary for the kernel residing in
~/kraken/reflex/coq/bench-<name>, simply run
cd ~/kraken/reflex make build NAME=<name>
Place your kernel in
~/kraken/reflex/coq/bench-<name>. Under that directory, run
ln -s ../Makefile.bench Makefile cd ~/kraken/reflex make build NAME=<name>
The resulting binary will reside in
~/kraken/reflex/coq/bench-<name>/ml/kernel. If you want to check the policies for that kernel using our proof automation, run
cd ~/kraken/reflex/coq/bench-<name> make policies
The root of the source code is at
~/kraken (kraken is an old name for the project). The implementation of the interpreter is located at
~/kraken/reflex/coq. A description of some of the files under that directory is given at
The kernels for the web browser, ssh server, and web server are located at
As described in the paper, the Reflex frontend is written in python. The implementation is at
~/kraken/reflex/coq/parser_ply.py. A discussion of why we choose to implement the frontend in python is provided in