ARTIFACT CORRESPONDING TO THE PAPER:

  Aaron Turon, Viktor Vafeiadis, and Derek Dreyer.
  GPS: Navigating weak memory with ghosts, protocols, and separation.

GETTING STARTED:

1. The artifact for our GPS paper is a mechanized proof of soundness
of our logic wrt the C11 model, as described in the paper and
appendix.  The artifact consists of approximately 7000 lines of Coq
code.

2. To test out this artifact, please download and run the free
VirtualBox application (https://www.virtualbox.org/) on the bootable VM image
gpsvm.ova.

3. When you boot up the virtual machine, there will be a file called
"Instructions" on the Desktop.  It provides step-by-step instructions
on how to verify that our mechanization passes the Coq proof checker.