@article{ladkin1999a,
author = {Ladkin, Peter and Lamport, Leslie and Olivier, Bryan and Roegel, Denis},
title = {A Lazy Caching Proof in TLA},
year = {1999},
month = {April},
abstract = {At some gathering (I believe it was the workshop where I presented [103]), Rob Gerth told me that he was compiling a collection of proofs of the lazy caching algorithm of Afek, Brown, and Merritt. I decided that this was a good opportunity to demonstrate the virtues of TLA, so there should be a TLA solution. In particular, I wanted to show that the proof is a straightforward engineering task, not requiring any new theory. I wanted to write a completely formal, highly detailed structured proof, but I didn't want to do all that dull work myself. So, I enlisted Ladkin, Olivier (who was then a graduate student of Paul Vitanyi in Amsterdam), and Roegel (who was then a graduate student of Dominique Mery in Nancy), and divided the task among them. However, writing a specification and proof is a process of continual refinement until everything fits together right. Getting this done in a long-distance collaboration is not easy, and we got tired of the whole business before a complete proof was written. However, we had done enough to write this paper, which contains specifications and a high-level overview of the proof.},
url = {http://approjects.co.za/?big=en-us/research/publication/lazy-caching-proof-tla/},
pages = {151-174},
journal = {Distributed Computing 12},
volume = {2},
number = {3},
}