Proofs for Adaptive Linear-Space Renaming

Proofs for Adaptive Linear-Space Renaming

Last modified 28 February 2017
The paper Adaptive Linear-Space Renaming by Delporte-Gallet, Fauconnier, Gafni, and Lamport appeared in Proceedings of the 27th International Symposium on Distributed Computing (DISC 2013).   Its algorithms were written in PlusCal and specified in PlusCal and TLA+.   Formal TLA+ proofs of their safety properties were written.   They were completely checked by TLAPS, the TLA+ Proof System. except that: Click here for a zip file containing the specifications.

The proofs are best read hierarchically using the TLA Toolbox.

Stephan Merz aided in writing the TLAPS proofs.


Contact Us Terms of Use Trademarks Privacy Statement ©2010 Microsoft Corporation. All rights reserved.Microsoft