Aquinas Hobor
Barriers in Separation Logic
Aquinas Hobor and Cristian Gherghina
Paper, submission version: (PDF)
Code, v0.1 (submission version
modulo some comments regarding copyright)
Note that the proof scripts require the
Mechanized Semantic
Library, v0.2.
Please contact Aquinas if there are troubles making the files
build.
License
It is our intention to release a cleaned-up version under a BSD-style license shortly.
However, until that time:
These proofs are (c) 2010
Aquinas Hobor, Cristian Gherghina, and Christopher Chak
All Rights Reserved.
Permission granted only to examine these proofs for the purpose
of evaluating the paper "Barriers in Separation Logic".
These proofs include a small portion of code (< 300 lines) from
the Concurrent C minor project in file SLB_Base.v; this portion
has been demarked by comments. The Concurrent C minor
portion is (c) 2007-2010 Andrew W. Appel, Robert Dockins, and
Aquinas Hobor. Permission granted only to use these lines
for the purpose of evaluating "Barriers in Separation Logic".