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.


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".

web site by Lucy Day Hobor ~ 2008-2020