Abstract : 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.
https://hal.inria.fr/inria-00098997
Contributeur : Publications Loria
<>
Soumis le : mardi 26 septembre 2006 - 08:41:03
Dernière modification le : mardi 24 avril 2018 - 13:34:29
