@inproceedings{Gra94,
title = { Verification of a distributed Cache memory by using abstractions },
author = {Graf, Susanne},
month = {jun},
year = {1994},
booktitle = {Conference on Computer Aided Verification CAV'94, Stanford},
note = {a largely improved and extended version appeared in Distributed Computing which is the online version},
publisher = {Springer Verlag},
series = {LNCS},
volume = {818},
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>) },
}
