Verified Compilation of Linearizable Data Structures

Mechanizing Rely Guarantee for Semantic Refinement

Accepted paper at the Software Verification and Testing track at the 33rd ACM/SIGAPP Symposium on Applied Computing.


Source code of the Coq formalization

Download the Coq development.

The development is known to compile with Coq 8.4pl6 (January 2016).

The development requires the ppsimpl tactic as a dependency, whose sources can be found: here.

To install ppsimpl:

Our formal development is organised as follow: