{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:21:53Z","timestamp":1725664913907},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602750"},{"type":"electronic","value":"9783540447849"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60275-5_57","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:06:20Z","timestamp":1330279580000},"page":"58-74","source":"Crossref","is-referenced-by-count":1,"title":["On the refinement of symmetric memory protocols"],"prefix":"10.1007","author":[{"given":"J. -P.","family":"Bodeveix","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Filali","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"issue":"4","key":"5_CR1","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/6513.6514","volume":"4","author":"J. Archibald","year":"1986","unstructured":"J. Archibald and J.-L. Baer. Cache coherence protocols: Evaluation using a multiprocessor simulation model. ACM Transactions on Computer Systems, 4(4):273\u2013298, nov 1986.","journal-title":"ACM Transactions on Computer Systems"},{"doi-asserted-by":"crossref","unstructured":"F. Andersen, K. D. Petersen, and J.S. Pettersson. Program verification using HOL-UNITY. In Higher Order Logic Theorem Proving and its Applications, volume 780 of Lecture Notes in Computer Science. Springer-Verlag, 1993.","key":"5_CR2","DOI":"10.1007\/3-540-57826-9_121"},{"key":"5_CR3","first-page":"389","volume-title":"volume 197 of Lecture Notes in Computer Science","author":"G. Berry","year":"1984","unstructured":"G. Berry and L. Cosserat. The ESTEREL synchronous programming language and its mathematical semantics. volume 197 of Lecture Notes in Computer Science, pages 389\u2013448, Berlin, Germany, 1984. Springer-Verlag."},{"doi-asserted-by":"crossref","unstructured":"J.-P. Bodeveix, M. Filali, and P. Roche. Towards a HOL theory of memory. In Higher Order Logic Theorem Proving and its Applications, volume 859 of Lecture Notes in Computer Science, pages 49\u201364. Springer-Verlag, sep 1994.","key":"5_CR4","DOI":"10.1007\/3-540-58450-1_34"},{"doi-asserted-by":"crossref","unstructured":"K.M. Chandy and J. Misra. Parallel Program Design, A Foundation. Addison-Wesley, 1988.","key":"5_CR5","DOI":"10.1007\/978-1-4613-9668-0_6"},{"doi-asserted-by":"crossref","unstructured":"C. Ching-Tsun. Mechanical verification of distributed algorithms in higher order logic. In Higher Order Logic Theorem Proving and its Applications, volume 859 of Lecture Notes in Computer Science, pages 158\u2013176. Springer-Verlag, 1994.","key":"5_CR6","DOI":"10.1007\/3-540-58450-1_41"},{"key":"5_CR7","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"E.W. Dijkstra. A Discipline of Programming. Englewood Cliffs New Jersey: Prentice Hall, 1976."},{"key":"5_CR8","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","unstructured":"J.-Y. Girard. Linear logic. Theoretical Comp. Science, 50:1\u2013102, 1987.","journal-title":"Theoretical Comp. Science"},{"unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL. Cambridge University Press, 1994.","key":"5_CR9"},{"doi-asserted-by":"crossref","unstructured":"C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.","key":"5_CR10","DOI":"10.1007\/978-3-642-82921-5_4"},{"unstructured":"D. Litaize. Architectures multiprocesseurs \u00e0 m\u00e9moire commune. In Deuxi\u00e8me symposium architectures nouvelles de machines, pages 1\u201340, sep 1990.","key":"5_CR11"},{"doi-asserted-by":"crossref","unstructured":"N.A. Lynch and M.R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the sixth annual ACM symposium on principles of distributed computing, pages 137\u2013151, aug 1987.","key":"5_CR12","DOI":"10.1145\/41840.41852"},{"doi-asserted-by":"crossref","unstructured":"F. Pong and M. Dubois. The verification of cache coherence protocols. Technical Report CENG-92-20, USC, nov 1992.","key":"5_CR13","DOI":"10.1145\/165231.165233"},{"issue":"6","key":"5_CR14","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1109\/2.55497","volume":"23","author":"P. Stenstrom","year":"1990","unstructured":"P. Stenstrom. A survey of cache coherence schemes for mutliprocessors. Computer, 23(6):11\u201325, jun 1990.","journal-title":"Computer"},{"unstructured":"G. Tredoux. Mechanizing execution sequence semantics in HOL. South African Computer Journal, (7), July 1992.","key":"5_CR15"},{"key":"5_CR16","volume-title":"PhD thesis","author":"J. Wright von","year":"1990","unstructured":"J. von Wright. A lattice-theoretical basis fro program refinement. PhD thesis, Abo Akademi Finland, 1990."}],"container-title":["Lecture Notes in Computer Science","Higher Order Logic Theorem Proving and Its Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60275-5_57.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T09:37:23Z","timestamp":1640943443000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60275-5_57"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602750","9783540447849"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-60275-5_57","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}