Mostly automated verification of higher-order programs with higher-order separation logic, with a small trusted code base http://plv.csail.mit.edu/bedrock/
This release requires Coq 8.4 (final released version).
Download coq-ext-lib from:
build it, and create a symbolic link called coq-ext-lib to that directory.
Download MirrorShard from:
build it, and create a symbolic link called mirror-shard to that directory.
Then, run one of the following:
make native
or
make ltac
to select whether to use the OCaml or Ltac reification code, respectively. By default, you get the Ltac version, which is much slower (i.e., adds hours to the time to build the library and all examples serially), but avoids the need to load a plugin into Coq, which can be tricky to do on some platforms.
Then, just run:
make
and go take a break while it runs for an hour or so (if you're lucky enough to have a new-ish machine). ;) Using the '-j' switch for parallel build is highly recommended.
Also see the 'examples' directory and its README.