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>) },


Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4001314