@article{Gra99,
title = { Characterization of a sequentially consistent memory and verification of a cache memory by abstraction },
author = {Graf, Susanne},
year = {1999},
note = {accepted for publication without any further revision since 1995},
journal = {Distributed Computing},
publisher = {Springer Verlag},
volume = {12},
team = {DCS},
abstract = {The contribution of the paper is two-fold. We give a set of properties expressible as temporal logic formulas such that any system satisfying them is a sequentially consistent memory, and which is sufficiently precise such that every reasonnable concrete system implementing a sequentially consistent memory satisfies these properties. Then, we verify these properties on a particular distributed cache memory systems by means of a verification method, based on the use of abstract interpretation which has been presented in previous papers (<A HREF=#LoiseauxGrafSifakisBouajjaniBensalem94> [LBBGS95]</A>) and often applied to finite state systems. The motivation of this paper was to show that it can also been applied to systems with infinite state space, and a more recent papers shows that the method can even be automatized (<A HREF=#GrafSaidi97>[GS97]</A>). This paper is a revised and extended version of (<A HREF=#graf94>[Graf94]</A>). },
}
