ISSN:
1432-0452
Source:
Springer Online Journal Archives 1860-2000
Topics:
Computer Science
Notes:
Summary. We address the problem, proposed by Gerth, of verifying that a simplified version of the lazy caching algorithm of Afek, Brown, and Merritt is sequentially consistent. We specify the algorithm and sequential consistency in TLA $^+$ , a formal specification language based on TLA (the Temporal Logic of Actions). We then describe how to construct and check a formal TLA correctness proof.
Type of Medium:
Electronic Resource
URL:
http://dx.doi.org/10.1007/s004460050063
Permalink