{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:50:09Z","timestamp":1754484609458,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540602477"},{"type":"electronic","value":"9783540447696"}],"license":[{"start":{"date-parts":[[1995,1,1]],"date-time":"1995-01-01T00:00:00Z","timestamp":788918400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0020472","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T08:33:05Z","timestamp":1132734785000},"page":"287-300","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Verifying distributed directory-based cache coherence protocols: S3.mp, a case study"],"prefix":"10.1007","author":[{"given":"Fong","family":"Pong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Nowatzyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gunes","family":"Aybay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michel","family":"Dubois","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Adve, S.V. and Hill, M.D., \u201cWeak Ordering\u2014A New Definition\u201d, Proc. of the 17th Int'l Symposium on Computer Architecture, May 1990, pp.2\u201314.","DOI":"10.1145\/325096.325100"},{"key":"24_CR2","unstructured":"Archibald, J., \u201cThe Cache Coherence Problem in Shared-Memory Multiprocessors\u201d, Ph.D Dissertation, University of Washington, Feb. 1987."},{"key":"24_CR3","unstructured":"Collier, W.W., Reasoning About Parallel Architectures, Prentice Hall, Englewood Cliffs, New Jersey."},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J. and Yang, C.H., \u201cProtocol Verification as a Hardware Design Aid\u201d, Int'l Conf. on Computer Design: VLSI in Computers and Processors, pp. 522\u2013525, Oct. 1992.","DOI":"10.1109\/ICCD.1992.276232"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J., \u201cAlgorithms for Automated Protocol Verification\u201d, AT&T Technical Journal, Jan.\/Feb. 1990.","DOI":"10.1002\/j.1538-7305.1990.tb00101.x"},{"key":"24_CR6","unstructured":"Ip, C.N. and Dill, D.L., \u201cBetter Verification Through Symmetry\u201d, Proc. 11th Int'l Symp. on Computer Hardwae Description Languages and Their Applications, pp. 87\u2013100, Apr. 1993."},{"key":"24_CR7","unstructured":"James et al., \u201cScalable Coherent Interface\u201d, IEEE Computer, June 90, Vol 23, No. 6, pp 71\u201382."},{"issue":"No.9","key":"24_CR8","doi-asserted-by":"crossref","first-page":"690","DOI":"10.1109\/TC.1979.1675439","volume":"C-28","author":"L. Lamport","year":"1979","unstructured":"Lamport, L., \u201cHow to Make a Multiprocessor Computer that Correctly Executes Multiprocess Programs\u201d, IEEE Trans. on Computers, Vol. C-28, No.9, Sept. 1979, pp.690\u2013691.","journal-title":"IEEE Trans. on Computers"},{"key":"24_CR9","doi-asserted-by":"crossref","unstructured":"Lenosky, D., et al., \u201cThe Directory-Based Cache Coherence Protocol for the DASH Multiprocessor\u201d, Proc. of the 17th Int'l Symposium on Computer Architecture, June 1990, pp. 148\u2013159.","DOI":"10.1145\/325096.325132"},{"key":"24_CR10","unstructured":"McMillan, K.L. and Schwalbe, J., \u201cFormal Verification of the Gigamax Cache Consistency Protocol\u201d, Proc. of the ISSM Int'l Conf. on Parallel and Distributed Computing, Oct. 1991."},{"key":"24_CR11","unstructured":"Nowaztyk, A. and Parkin, M., \u201cThe S3.mp Interconnection System and TIC Chip\u201d, Hot Interconnects 1993."},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Nowatzyk, A., Aybay, G., Browne, M., Kelly, E., Parkin, M., Radke, B. and Vishin, S., \u201cThe S3.mp Scalable Shared Memory Multiprocessor\u201d, HICCS, 1994.","DOI":"10.1109\/HICSS.1994.323149"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Pong, F. and Dubois, M., \u201cThe Verification of Cache Coherence Protocols\u201d, Proc. of the 5th Annual Symp. on Parallel Algorithm and Architecture, pp.11\u201320, June 1993.","DOI":"10.1145\/165231.165233"},{"key":"24_CR14","unstructured":"Pong, F. and Dubois, M., \u201cFormal Verification of Complex Coherence Protocols Using Symbolic State Models\u201d, Technical Report CENG-94-01, University of Southern California."},{"key":"24_CR15","volume-title":"Scalable Shared Memory Multiprocessors","author":"P.S. Sindhu","year":"1992","unstructured":"Sindhu, P.S., Frailong, J-M. and Cekleov, M., \u201cFormal Specification of Memory Models\u201d, In Dubois, M. and Thakkar, S., Editors. Scalable Shared Memory Multiprocessors. Kluwer, Norwell, MA, 1992."},{"issue":"No.6","key":"24_CR16","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1109\/2.55497","volume":"23","author":"P. Stenstr\u00f6m","year":"1990","unstructured":"Stenstr\u00f6m, P., \u201cA Survey of Cache Coherence Schemes for Multiprocessors\u201d, IEEE Computer, Vol. 23, No. 6, pp. 12\u201324, June 1990.","journal-title":"IEEE Computer"},{"key":"24_CR17","unstructured":"The SPARC Architecture Manual, Version 9, Prentice Hall."},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Thapar, M. and Delagi, B., \u201cStanford Distributed-Directory Protocol\u201d, IEEE Computer, June 1990, pp. 78\u201380.","DOI":"10.1109\/2.55504"}],"container-title":["Lecture Notes in Computer Science","EURO-PAR '95 Parallel Processing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0020472","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,5]],"date-time":"2025-01-05T21:45:52Z","timestamp":1736113552000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0020472"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540602477","9783540447696"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0020472","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]},"assertion":[{"value":"9 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}