Proofs for Adaptive Register Allocation with a Linear Number of Registers

Proofs for Adaptive Register Allocation with a Linear Number of Registers

Last modified 10 August 2013
The paper Adaptive Register Allocation with a Linear Number of Registers by Delporte-Gallet, Fauconner, Gafni, and Lamport will appear in the proceedings of DISC 2013.   Its algorithms are written in PlusCal and specified in PlusCal and TLA+.   Formal TLA+ proofs of their safety properties have been written.   They have been completely checked by the 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