{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:54Z","timestamp":1761611214199,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":28,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540646778"},{"type":"electronic","value":"9783540691082"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/3-540-69108-1_6","type":"book-chapter","created":{"date-parts":[[2007,8,6]],"date-time":"2007-08-06T18:45:11Z","timestamp":1186425911000},"page":"84-103","source":"Crossref","is-referenced-by-count":4,"title":["Modelling and Model Checking a Distributed Shared Memory Consistency Protocol"],"prefix":"10.1007","author":[{"given":"Kathi","family":"Fisler","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claude","family":"Girault","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,3,3]]},"reference":[{"issue":"12","key":"6_CR1","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1109\/2.546611","volume":"29","author":"S. V. Adve","year":"1996","unstructured":"Adve, S. V., Gharachorloo, K.: Shared Memory Consistency Models: A Tutorial. In IEEE Computer, 29,12 (Dec. 1996) 66\u201376","journal-title":"IEEE Computer"},{"key":"6_CR2","unstructured":"Baer, J-L., Girault, C.: A Petri net model for a solution to the cache coherence problem. In Proc. First International Conference on Supercomputing Systems, St Petersburg, Florida (1985) 680\u2013689"},{"key":"6_CR3","unstructured":"Barroso, L.A., Dubois, M.: Cache Coherence on a Slotted Ring. In IEEE Trans. on Computers, 44,7, Berlin, Germany (Sept. 1991)"},{"key":"6_CR4","unstructured":"Blondel, X., Rosenfeld, L., Ruget, F., Singhoff, F.: Exp\u00e9riences de Mise au Point d\u2019un Algorithme R\u00e9parti. To appear in Technique et Science Informatiques (1998)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Carter, J., Bennett, J., Zwaenepoel, W.: Implementation and Performance of Munin. In Proc. 13th ACM Symposium on Operating System Principles (1991) 152\u2013164","DOI":"10.1145\/121132.121159"},{"issue":"3","key":"6_CR6","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1145\/210126.210127","volume":"13","author":"J. Carter","year":"1995","unstructured":"Carter, J., Bennett, J., Zwaenepoel, W.: Techniques for Reducing Consistencyrelated Communication in Distributed Shared-memory Systems. ACM Trans. Comput. Syst. 13,3 (Aug. 1995) 205\u2013243","journal-title":"ACM Trans. Comput. Syst."},{"key":"6_CR7","series-title":"Lect Notes Comput Sci","first-page":"1","volume-title":"Proc. 7th European Workshop on Application and Theory of Petri nets","author":"C. Chatelain","year":"1987","unstructured":"Chatelain, C., Girault, C., Haddad, S.: Specification and Properties of a Cache Coherence Protocol Model. In Proc. 7th European Workshop on Application and Theory of Petri nets, Oxford England (June 1986), Advances in Petri nets 87, LNCS., Vol. 266, Springer-Verlag (1987) 1\u201320"},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1016\/S0304-3975(96)00010-2","volume":"176","author":"G. Chiola","year":"1997","unstructured":"Chiola, G., Dutheillet, C., Francheschinis, G., Haddad, S.: A Symbolic Reachability Graph for Coloured Petri Nets, Theoretical Computer Science, Vol. 176 (1997) 39\u201365","journal-title":"Theoretical Computer Science"},{"key":"6_CR9","unstructured":"Clarke, E., Grumberg, O., Hiraishi, H., Jha, S., Long, D., McMillan, K., Ness, L.: Verification of the Futurebus+ Cache Coherency Protocol. In Proc. Conf. on Computer Hardware Description Languages and their Application. North-Holland (1993)"},{"key":"6_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"51","DOI":"10.1007\/3-540-56689-9_39","volume-title":"Advances in Petri nets 87","author":"J.M. Couvreur","year":"1993","unstructured":"Couvreur, J.M., Haddad, S., Peyre, J.F.: Generative Families of Positive Invariants in Coloured Nets Sub-Classes. In Advances in Petri nets 87, LNCS., Vol. 674, Springer-Verlag (1993) 51\u201370"},{"key":"6_CR11","unstructured":"Golpalakrishnan, G., Khandekar, D., Kuramkote, R., Nalamasu, M.: Case Studies in Symbolic Model Checking: Verification of an Arbiter and DSM Protocols. Tech. Report UUCS-94-009, Dept. of Computer Science, Univ. of Utah (March 1994)"},{"key":"6_CR12","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"440","DOI":"10.1007\/3-540-63166-6_43","volume-title":"Proc. 9th Int\u2019l. Conf. on Computer-Aided Verification","author":"B. Grahlmann","year":"1997","unstructured":"Grahlmann, B.: The PEP Tool. In Proc. 9th Int\u2019l. Conf. on Computer-Aided Verification, Haifa, Israel, LNCS., Vol. 1254, Springer-Verlag (1997) 440\u2013443"},{"key":"6_CR13","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Proc. Int\u2019l. Conf. on Computer-Aided Verification","author":"R. H. Hardin","year":"1996","unstructured":"Hardin, R. H., Har\u2019El, Z., Kurshan, R.P.: COSPAN. In Proc. Int\u2019l. Conf. on Computer-Aided Verification, LNCS Vol., 1102, Springer-Verlag (1996) 423\u2013427"},{"key":"6_CR14","unstructured":"Holzmann, G.: Design and Validation of Computer Protocols, Prentice Hall (1991)"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Jensen, K. Rozenberg, G. (eds.): High Level Petri Nets, Theory and Applications, Springer-Verlag (1991)","DOI":"10.1007\/978-3-642-84524-6"},{"key":"6_CR16","unstructured":"Jensen, K.: Coloured Petri Nets: Basic Concepts, Analysis Methods and Practical Use, Vol. 1, 2 and 3, Springer-Verlag (1995)"},{"issue":"7","key":"6_CR17","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/BF00625967","volume":"9","author":"K. Jensen","year":"1996","unstructured":"Jensen, K.: Condensed State Spaces for Symmetrical Coloured Petri Nets, Formal Methods in System Design, Vol. 9,7 (1996) 7\u201340","journal-title":"Formal Methods in System Design"},{"key":"6_CR18","doi-asserted-by":"crossref","unstructured":"Keheler, P.: The Relative Importance of Concurrent Writers and Weak Consistency Models. In Proc. 16th Int\u2019l Conf. on Distributed Computing Systems, IEEE Computer Society Press (May 1992) 91\u201398","DOI":"10.1109\/ICDCS.1996.507905"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Keheler, P., Cox, A.L., Zwaenepoel, W.: Lazy Release Consistency for Software Distributed Shared Memory. In Proc. 19th Annual Int\u2019l Symposium on Computer Architecture (May 1992) 13\u201321","DOI":"10.1145\/146628.139676"},{"key":"6_CR20","unstructured":"Li, K.: Shared Virtual Memory on Loosely Coupled Multiprocessors. PhD dissertation, Dept. of Computer Science, Yale University, New Haven, Conn., Tech Rep YALEU-RR-492 (May 1992)"},{"key":"6_CR21","first-page":"94","volume":"II","author":"K. Li","year":"1988","unstructured":"Li, K.: IVY: A Shared Virtual Memory System for Parallel Computing. In Proc. 1988 Int\u2019l Conf. on Parallel Processing, Vol. II (1988) 94\u2013101","journal-title":"Proc. 1988 Int\u2019l Conf. on Parallel Processing"},{"issue":"4","key":"6_CR22","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1145\/75104.75105","volume":"7","author":"K. Li","year":"1989","unstructured":"Li, K. Hudak, P: Memory Coherence in Shared Virtual Memory Systems. ACM Trans. on Computer Systems, Vol. 7,4 (Nov. 1989) 321\u2013359","journal-title":"ACM Trans. on Computer Systems"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Lindemann, C., Sch\u00f6n, F.: Modeling Relaxed Memory Consistency Protocols. In Proc. 8th Int\u2019l Conf. on Modelling Techniques and Tools for Computer Systems Performance Evaluation, Heidelberg, Germany (Sept 1995)","DOI":"10.1007\/BFb0024329"},{"issue":"1\/2","key":"6_CR24","first-page":"41","volume":"9","author":"C. N. Ip","year":"1996","unstructured":"Ip, C. N., Dill, D.: Better Verification Through Symmetry. In Formal Methods in System Design, Vol. 9,1\/2 (1996) 41\u201376","journal-title":"Formal Methods in System Design"},{"issue":"1","key":"6_CR25","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1145\/248621.248624","volume":"29","author":"F. Pong","year":"1997","unstructured":"Pong, F. Dubois, M.: Verification Techniques for Cache Coherence Protocols. ACM Computing Surveys, Vol. 29,1, (March 1997) 82\u2013126","journal-title":"ACM Computing Surveys"},{"issue":"1","key":"6_CR26","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/358527.358537","volume":"24","author":"G. Ricart","year":"1981","unstructured":"Ricart, G. Agrawala, A.: An Optimal Algorithm for Mutual Exclusion. Comm. ACM, Vol. 24,1, (Jan. 1981) 9\u201317","journal-title":"Comm. ACM"},{"issue":"4","key":"6_CR27","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1145\/6110.214406","volume":"3","author":"I. Suzuki","year":"1985","unstructured":"Suzuki, I. Kasami, T.: A Distributed Mutual Exclusion Algorithm. ACM Trans. on Computer Systems, Vol. 3,4 (Nov 1985) 344\u2013349","journal-title":"ACM Trans. on Computer Systems"},{"key":"6_CR28","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"472","DOI":"10.1007\/3-540-63166-6_51","volume-title":"Proc. 9th Int\u2019l. Conf. on Computer-Aided Verification","author":"K. Varpaaniemi","year":"1997","unstructured":"Varpaaniemi, K., Heljanko, K., Lilius, J.: Prod 3.2-An Advanced Tool for Efficient Reachability Analysis, In Proc. 9th Int\u2019l. Conf. on Computer-Aided Verification, Haifa, Israel, LNCS, Vol. 1254, Springer-Verlag (1997) 472\u2013475"}],"container-title":["Lecture Notes in Computer Science","Application and Theory of Petri Nets 1998"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-69108-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,20]],"date-time":"2025-01-20T04:42:02Z","timestamp":1737348122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-69108-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540646778","9783540691082"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/3-540-69108-1_6","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1998]]}}}