{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T06:04:53Z","timestamp":1790057093529,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540677703","type":"print"},{"value":"9783540450474","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722167_8","type":"book-chapter","created":{"date-parts":[[2006,12,30]],"date-time":"2006-12-30T03:00:33Z","timestamp":1167447633000},"page":"53-68","source":"Crossref","is-referenced-by-count":94,"title":["Automatic Verification of Parameterized Cache Coherence Protocols"],"prefix":"10.1007","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla, P.A., Cer\u0101ns, K., Jonsson, B., Tsay, Y.-K.: General Decidability Theorems for Infinite-State Systems. In: Proc. 10th IEEE Int. Symp. on Logic in Computer Science, pp. 313\u2013321 (1996)","DOI":"10.1109\/LICS.1996.561359"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"1999","unstructured":"Abdulla, P.A., Bouajjani, A., Jonsson, B., Nilsson, M.: Handling Global Conditions in Parameterized System Verification. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 134\u2013145. Springer, Heidelberg (1999)"},{"key":"8_CR3","unstructured":"Abdulla, P.A., Jonsson, B.: Ensuring Completeness of Symbolic Verification Methods for Infinite-State Systems. To appear in Theoretical Computer Science (1999)"},{"issue":"4","key":"8_CR4","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/6513.6514","volume":"4","author":"P.A. Archibald","year":"1986","unstructured":"Archibald, P.A., Baer, J.: Cache Coherence Protocols: Evaluation Using a Multiprocessor Simulation Model. ACM Transactions on Computer Systems\u00a04(4), 273\u2013298 (1986)","journal-title":"ACM Transactions on Computer Systems"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"400","DOI":"10.1007\/3-540-63166-6_39","volume-title":"Computer Aided Verification","author":"T. Bultan","year":"1997","unstructured":"Bultan, T., Gerber, R., Pugh, W.: Symbolic Model Checking of Infinitestate Systems using Presburger Arithmetics. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 400\u2013411. Springer, Heidelberg (1997)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/BFb0028736","volume-title":"Computer Aided Verification","author":"B. Boigelot","year":"1998","unstructured":"Boigelot, B., Wolper, P.: Verifying Systems with Infinite but Regular State Space. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 88\u201397. Springer, Heidelberg (1998)"},{"issue":"1","key":"8_CR7","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"Browne, M.C., Clarke, E.M., Grumberg, O.: Reasoning about Networks with Many Identical Finite State Processes. Information and Computation\u00a081(1), 13\u201331 (1989)","journal-title":"Information and Computation"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1145\/225871.225880","volume":"1","author":"K.-T. Cheng","year":"1996","unstructured":"Cheng, K.-T., Krishnakumar, A.S.: Automatic Generation of Functional Vectors Using the Extended Finite State Machine Model. ACM Transactions on Design Automation of Electronic Systems\u00a01(1), 57\u201379 (1996)","journal-title":"ACM Transactions on Design Automation of Electronic Systems"},{"key":"8_CR9","unstructured":"Clarke, E.M., Grumberg, O., Hiraishi, H., Jha, S., Long, D.E., McMillan, K.L., Ness, L.A.: Verification of the Futurebus+cache coherence protocol. In: Proc. 11th Int. Symp. on Computer Hardware Description Languages and their Applications (1993)"},{"issue":"5","key":"8_CR10","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1145\/265943.265960","volume":"19","author":"E. Clarke","year":"1997","unstructured":"Clarke, E., Grumberg, O., Jha, S.: Verifying Parameterized Networks. TOPLAS\u00a019(5), 726\u2013750 (1997)","journal-title":"TOPLAS"},{"key":"8_CR11","unstructured":"Delzanno, G.: On Efficient Data Structures for the Verification of Parameterized Synchronous Systems. Tech. Rep. DISI-00-03, Dip. di Informaticae Scienze dell\u2019Informazione, Universit\u00e0 di Genova (January 2000)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-48168-0_5","volume-title":"Computer Science Logic","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Esparza, J., Podelski, A.: Constraint-based Analysis of Broadcast Protocols. In: Flum, J., Rodr\u00edguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol.\u00a01683, pp. 50\u201366. Springer, Heidelberg (1999)"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-49059-0_16","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"G. Delzanno","year":"1999","unstructured":"Delzanno, G., Podelski, A.: Model Checking in CLP. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 223\u2013239. Springer, Heidelberg (1999)"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/3-540-61474-5_60","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Namjoshi, K.S.: Automatic Verification of Parameterized Synchronous Systems. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 87\u201398. Springer, Heidelberg (1996)"},{"key":"8_CR15","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Namjoshi, K.S.: On Model Checking for Nondeterministic Infinite-state Systems. In: Proc. of the 13th Annual Symp. on Logic in Computer Science (LICS 1998), pp. 70\u201380 (1998)","DOI":"10.1109\/LICS.1998.705644"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/BFb0028766","volume-title":"Computer Aided Verification","author":"E.A. Emerson","year":"1998","unstructured":"Emerson, E.A., Namjoshi, K.S.: Verification of Parameterized Bus Arbitration Protocol. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 452\u2013463. Springer, Heidelberg (1998)"},{"key":"8_CR17","doi-asserted-by":"crossref","unstructured":"Esparza, J., Finkel, A., Mayr, R.: On the Verification of Broadcast Protocols. In: Proc. 14th Annual Symp. on Logic in Computer Science (LICS 1999), pp. 352\u2013359 (1999)","DOI":"10.1109\/LICS.1999.782630"},{"key":"#cr-split#-8_CR18.1","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Tech. Rep. LSV-98-4, Lab. Specification et Verification, ENS de Cachan (April 1998);"},{"key":"#cr-split#-8_CR18.2","unstructured":"To appear in Theoretical Computer Science"},{"issue":"3","key":"8_CR19","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"German, S.M., Sistla, A.P.: Reasoning about Systems with Many Processes. JACM\u00a039(3), 675\u2013735 (1992)","journal-title":"JACM"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of Abstract State Graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_10"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/3-540-56922-7_28","volume-title":"Computer Aided Verification","author":"N. Halbwachs","year":"1993","unstructured":"Halbwachs, N.: Delay Analysis in Synchronous Programs. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 333\u2013346. Springer, Heidelberg (1993)"},{"key":"8_CR22","volume-title":"The Cache Memory Book","author":"J. Handy","year":"1993","unstructured":"Handy, J.: The Cache Memory Book. Academic Press, London (1993)"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"252","DOI":"10.1007\/3-540-60472-3_13","volume-title":"Hybrid Systems II","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H.: A Note on Abstract-interpretation Strategies for Hybrid Automata. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol.\u00a0999, pp. 252\u2013264. Springer, Heidelberg (1995)"},{"key":"8_CR24","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Hytech: a Model Checker for Hybrid Systems. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 460\u2013463. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_48"},{"key":"8_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/3-540-48683-6_27","volume-title":"Computer Aided Verification","author":"T.A. Henzinger","year":"1999","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 301\u2013315. Springer, Heidelberg (1999)"},{"issue":"3","key":"8_CR26","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1023\/A:1008723125149","volume":"14","author":"C. Norris Ip","year":"1999","unstructured":"Norris Ip, C., Dill, D.L.: Verifying Systems with Replicated Components in Murphi. Formal Methods in System Design\u00a014(3), 273\u2013310 (1999)","journal-title":"Formal Methods in System Design"},{"key":"8_CR27","doi-asserted-by":"crossref","unstructured":"Lesens, D., Halbwachs, N., Raymond, P.: Automatic Verification of Parameterized Linear Networks of Processes. In: Proc. 24th ACM Symposium on Principles of Programming Languages (POPL 1997), pp. 346\u2013357 (1997)","DOI":"10.1145\/263699.263747"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Verification of Infinite State Systems by Compositional Model Checking. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 219\u2013237. Springer, Heidelberg (1999)","DOI":"10.1007\/3-540-48153-2_17"},{"key":"8_CR29","unstructured":"McMillan, K.L., Schwalbe, J.: Formal Verification of the Gigamax Cache Consistency Protocol. In: Proc. Int. Symp. on Shared Memory Multiprocessors, pp. 242\u2013251 (1991)"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"Papamarcos, M.S., Patel, J.H.: A Low-Overhead Coherence Solution for Multiprocessors with Private Cache Memories. In: Proc. Int. Symp. onComputer Architecture (ISCA 1984), pp. 348\u2013354 (1984)","DOI":"10.1145\/800015.808204"},{"key":"8_CR31","doi-asserted-by":"crossref","unstructured":"Pong, F., Dubois, M.: A New Approach for the Verification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems\u00a06(8) (1995)","DOI":"10.1109\/71.406955"},{"issue":"1","key":"8_CR32","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\u00a029(1), 82\u2013126 (1997)","journal-title":"ACM Computing Surveys"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722167_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T19:06:43Z","timestamp":1736708803000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722167_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677703","9783540450474"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/10722167_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000]]}}}