{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T06:04:10Z","timestamp":1790057050444,"version":"4.0.1"},"reference-count":44,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2003,11,1]],"date-time":"2003-11-01T00:00:00Z","timestamp":1067644800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2003,11,1]],"date-time":"2003-11-01T00:00:00Z","timestamp":1067644800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2003,11]]},"DOI":"10.1023\/a:1026276129010","type":"journal-article","created":{"date-parts":[[2003,11,3]],"date-time":"2003-11-03T17:53:28Z","timestamp":1067882008000},"page":"257-301","source":"Crossref","is-referenced-by-count":47,"title":["Constraint-Based Verification of Parameterized Cache Coherence Protocols"],"prefix":"10.1007","volume":"23","author":[{"given":"Giorgio","family":"Delzanno","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5146977_CR1","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson, \u201cHandling global conditions in parameterized system verification,\u201d in N. Halbwachs and D. Peled (Eds.), Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99), Lecture Notes in Computer Science, Trento, Italy, 1999, Vol. 1633, pp. 134\u2013145.","DOI":"10.1007\/3-540-48683-6_14"},{"key":"5146977_CR2","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla, K. Cer\u00e3ns, B. Jonsson, and Y.-K. Tsay, \u201cGeneral decidability theorems for infinite-state systems,\u201d in Proceedings of the 11th Annual International Symposium on Logic in Computer Science (LICS\u2019 96), New Brunswick, New Jersey, 1996, pp. 313\u2013321.","DOI":"10.1109\/LICS.1996.561359"},{"issue":"1\/2","key":"5146977_CR3","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/S0304-3975(00)00105-5","volume":"256","author":"P.A. Abdulla","year":"2001","unstructured":"P.A. Abdulla and B. Jonsson, \u201cEnsuring completeness of symbolic verification methods for infinite-state systems,\u201d Theoretical Computer Science, Vol. 256, Nos. 1\/2, pp. 145\u2013167, 2001.","journal-title":"Theoretical Computer Science"},{"key":"5146977_CR4","doi-asserted-by":"crossref","unstructured":"P.A. Abdulla and A. Nyl\u00e9 n, \u201cBetter is better than well: On efficient verification of infinite-state systems,\u201d in Proceedings of the 15th Annual International Symposium on Logic in Computer Science (LICS\u2019 00), Santa Barbara, California, 2000, pp. 132\u2013140.","DOI":"10.1109\/LICS.2000.855762"},{"issue":"4","key":"5146977_CR5","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1145\/6513.6514","volume":"4","author":"P.A. Archibald","year":"1986","unstructured":"P.A. Archibald and J. Baer, \u201cCache coherence protocols: Evaluation using a multiprocessor simulation model,\u201d ACM Transactions on Computer Systems, Vol. 4, No. 4, pp. 273\u2013298, 1986.","journal-title":"ACM Transactions on Computer Systems"},{"key":"5146977_CR6","doi-asserted-by":"crossref","unstructured":"T. Arons, A. Pnueli, S. Ruah, Y. Xu, and L.D. Zuck, \u201cParameterized verification with automatically computed inductive assertions,\u201d in G. Berry, H. Comon, and A. Finkel (Eds.), Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u2019 01), Lecture Notes in Computer Science, Paris, France, 2001, Vol. 2102, pp. 221\u2013234.","DOI":"10.1007\/3-540-44585-4_19"},{"key":"5146977_CR7","first-page":"204","volume":"1785","author":"J.-P. Bodeveix","year":"2000","unstructured":"J.-P. Bodeveix and M. Filali, \u201cFMona: A tool for expressing validation techniques over infinite state systems,\u201d in Proceedings of the 6th Int. Con. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 00), Lecture Notes in Computer Science, Berlin, Germany, 2000, Vol. 1785, pp. 204\u2013218.","journal-title":"Proceedings of the 6th Int. Con. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u2019 00), Lecture Notes in Computer Science"},{"key":"5146977_CR8","first-page":"88","volume":"1427","author":"B. Boigelot","year":"1998","unstructured":"B. Boigelot and P. Wolper, \u201cVerifying systems with infinite but regular state space,\u201d in Proceedings of the 10th Conf. on Computer Aided Verification (CAV\u2019 98), Lecture Notes in Computer Science, 1998, Vol. 1427, pp. 88\u201397.","journal-title":"Proceedings of the 10th Conf. on Computer Aided Verification (CAV\u2019 98), Lecture Notes in Computer Science"},{"key":"5146977_CR9","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili, \u201cRegular model checking,\u201d in E.A. Emerson and A.P. Sistla (Eds.), Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00), Lecture Notes in Computer Science, Chicago, Illinois, 2000, Vol. 1855, pp. 403\u2013418.","DOI":"10.1007\/10722167_31"},{"issue":"1","key":"5146977_CR10","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1016\/0890-5401(89)90026-6","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg, \u201cReasoning about networks with many identical finite state processes,\u201d Information and Computation, Vol. 81, No. 1, pp. 13\u201331, 1989.","journal-title":"Information and Computation"},{"key":"5146977_CR11","doi-asserted-by":"crossref","unstructured":"T. Bultan, R. Gerber, and W. Pugh, \u201cSymbolic model checking of infinite state systems using presburger arithmetics,\u201d in O.Grumberg (Ed.), Proceedings 9th International Conference on Computer Aided Verification (CAV\u2019 97), Lecture Notes in Computer Science, Haifa, Israel, 1997, Vol. 1254, pp. 400\u2013411.","DOI":"10.1007\/3-540-63166-6_39"},{"issue":"1","key":"5146977_CR12","doi-asserted-by":"crossref","first-page":"57","DOI":"10.1145\/225871.225880","volume":"1","author":"K.-T. Cheng","year":"1996","unstructured":"K.-T. Cheng and A.S. Krishnakumar, \u201cAutomatic generation of functional vectors using the extended finite state machine model,\u201d ACM Transactions on Design Automation of Electronic Systems, Vol. 1, No. 1, pp. 57\u201379, 1996.","journal-title":"ACM Transactions on Design Automation of Electronic Systems"},{"issue":"5","key":"5146977_CR13","doi-asserted-by":"crossref","first-page":"726","DOI":"10.1145\/265943.265960","volume":"19","author":"E. Clarke","year":"1997","unstructured":"E. Clarke, O. Grumberg, and S. Jha, \u201cVerifying parameterized networks,\u201d TOPLAS, Vol. 19, No. 5, pp. 726\u2013750, 1997.","journal-title":"TOPLAS"},{"key":"5146977_CR14","unstructured":"E.M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D.E. Long, K.L. McMillan, and L.A. Ness, \u201cVerification of the futurebus + cache coherence protocol,\u201d in L.J.M.C.D. Agnew and R. Camposano (Eds.), Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications (CHDL\u2019 93), sponsored by IFIP WG10.2 and in cooperation with IEEE COMPSOC, Ottawa, Ontario, Canada, 1993, pp. 15\u201330."},{"key":"5146977_CR15","doi-asserted-by":"crossref","unstructured":"G. Delzanno, \u201cAutomatic verification of parameterized cache coherence protocols,\u201d in E.A. Emerson and A.P. Sistla (Eds.), Proceedings of the 12th International Conference on Computer Aided Verification (CAV\u2019 00), Lecture Notes in Computer Science, Chicago, Illinois, Vol. 1855, 2000.","DOI":"10.1007\/10722167_8"},{"key":"5146977_CR16","doi-asserted-by":"crossref","unstructured":"G. Delzanno and T. Bultan, \u201cConstraint-based verification of client-server protocols,\u201d in T. Walsh (Ed.), Proceedings of the 7th International Conference on Principles and Practice of Constraint Programming (CP\u2019 01), Lecture Notes in Computer Science, Paphos, Cyprus, 2001, Vol. 2239, pp. 286\u2013301.","DOI":"10.1007\/3-540-45578-7_20"},{"key":"5146977_CR17","doi-asserted-by":"crossref","unstructured":"G. Delzanno, J. Esparza, and A. Podelski, \u201cConstraint-based analysis of broadcast protocols,\u201d in J. Flum and M. Rodr\u00cdguez-Artalejo (Eds.), Proceedings of the 1999 Annual Conference of the European Association for Computer Science Logic (CSL\u2019 99), Lecture Notes in Computer Science, Madrid, Spain, pp. 50\u201366, 1999, Vol. 1683.","DOI":"10.1007\/3-540-48168-0_5"},{"key":"5146977_CR18","doi-asserted-by":"crossref","unstructured":"G. Delzanno and A. Podelski, \u201cModel checking in CLP,\u201d in R. Cleaveland (Ed.), Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS\u2019 99), Lecture Notes in Computer Science, Amsterdam, The Netherlands, 1999, Vol. 1579, pp. 223\u2013239.","DOI":"10.1007\/3-540-49059-0_16"},{"key":"5146977_CR19","doi-asserted-by":"crossref","unstructured":"G. Delzanno, J.-F. Raskin, and L.V. Begin, \u201cAttacking symbolic state explosion,\u201d in G. Berry, H. Comon, and A. Finkel (Eds.), Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u2019 01), Lecture Notes in Computer Science, Paris, France, 2001, Vol. 2102, pp. 298\u2013310.","DOI":"10.1007\/3-540-44585-4_28"},{"key":"5146977_CR20","doi-asserted-by":"crossref","unstructured":"E. Emerson and K. Namjoshi, \u201cOn model checking for non-deterministic infinite-state systems,\u201d in Proceedings of the 13th International Symposium on Logic in Computer Science (LICS\u2019 98), Indianapolis, Indiana, 1998, pp. 70\u201380.","DOI":"10.1109\/LICS.1998.705644"},{"key":"5146977_CR21","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, and R. Mayr, \u201cOn the verification of broadcast protocols,\u201d in Proceedings 14th International Symposium on Logic in Computer Science (LICS\u2019 99), Trento, Italy, 1999, pp. 352\u2013359.","DOI":"10.1109\/LICS.1999.782630"},{"issue":"1\/2","key":"5146977_CR22","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"A. Finkel and P. Schnoebelen, \u201cWell-structured transition systems everywhere,\u201d Theoretical Computer Science, Vol. 256, Nos. 1\/2, pp. 63\u201392, 2001.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"5146977_CR23","doi-asserted-by":"crossref","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"S.M. German","year":"1992","unstructured":"S.M. German and A.P. Sistla, \u201cReasoning about systems with many processes,\u201d Journal of the ACM, Vol. 39, No. 3, pp. 675\u2013735, 1992.","journal-title":"Journal of the ACM"},{"issue":"2\/3","key":"5146977_CR24","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/s004460050059","volume":"12","author":"S. Graf","year":"1999","unstructured":"S. Graf, \u201cCharacterization of a sequentially consistent memory and verification of a cache memory by abstraction,\u201d Distributed Computing, Vol. 12, Nos. 2\/3, pp. 75\u201390, 1999.","journal-title":"Distributed Computing"},{"key":"5146977_CR25","unstructured":"S. Graf and H. Sa\u00efdi, \u201cConstruction of abstract state graphs with PVS,\u201d in O. Grumberg (Ed.), Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97), Lecture Notes in Computer Science, Haifa, Israel, 1997, Vol. 1254, pp. 72\u201383."},{"key":"5146977_CR26","doi-asserted-by":"crossref","unstructured":"N. Halbwachs, \u201cDelay analysis in synchronous programs,\u201d in C. Courcoubetis (Ed.), Proceedings of the 5th Conference on Computer-Aided Verification (CAV'93), Lecture Notes in Computer Science, Elounda, Greece, 1993, Vol. 697, pp. 333\u2013346.","DOI":"10.1007\/3-540-56922-7_28"},{"key":"5146977_CR27","unstructured":"J. Handy, The Cache Memory Book, Academic Press, 1993."},{"key":"5146977_CR28","first-page":"460","volume-title":"Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97), Lecture Notes in Computer Science","author":"T.A. Henzinger","year":"1997","unstructured":"T.A. Henzinger, P.-H. Ho, and H.Wong-Toi, \u201cHYTECH: A model checker for hybrid systems,\u201d in O. Grumberg (Ed.), Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97), Lecture Notes in Computer Science, Springer, Haifa, Israel, 1997, Vol. 1254, pp. 460\u2013463."},{"key":"5146977_CR29","first-page":"301","volume-title":"Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99), Lecture Notes in Computer Science","author":"T.A. Henzinger","year":"1999","unstructured":"T.A. Henzinger, S. Qadeer, and S.K. Rajamani, \u201cVerifying sequential consistency on shared-memory multiprocessor systems,\u201d in N. Halbwachs and D. Peled (Eds.), Proceedings of the 11th International Conference on Computer Aided Verification (CAV'99), Lecture Notes in Computer Science. Trento, Italy: Springer, 1999, Vol. 1633, pp. 301\u2013315."},{"issue":"2","key":"5146977_CR30","doi-asserted-by":"crossref","first-page":"147","DOI":"10.1016\/S0022-0000(69)80011-5","volume":"3","author":"R.M. Karp","year":"1969","unstructured":"R.M. Karp and R.E. Miller, \u201cParallel program schemata,\u201d Journal of Computer and System Sciences, Vol. 3, No. 2, pp. 147\u2013195, 1969.","journal-title":"Journal of Computer and System Sciences"},{"key":"5146977_CR31","doi-asserted-by":"crossref","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar, \u201cSymbolic model checking with rich assertional languages,\u201d in O. Grumberg (Ed.), Proceedings of the 9th International Conference on Computer Aided Verification (CAV'97), Lecture Notes in Computer Science, Haifa, Israel, 1997, Vol. 1254, pp. 424\u2013435.","DOI":"10.1007\/3-540-63166-6_41"},{"key":"5146977_CR32","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond, \u201cAutomatic verification of parameterized linear networks of processes,\u201d in Proceedings of the 24th Symposium on Principles of Programming Languages (POPL'97), Paris, France, 1997, pp. 346\u2013357.","DOI":"10.1145\/263699.263747"},{"key":"5146977_CR33","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/BF00289237","volume":"21","author":"B.D. Lubachevsky","year":"1984","unstructured":"B.D. Lubachevsky, \u201cAn approach to automating the verification of compact parallel coordination programs,\u201d Acta Informatica, Vol. 21, pp. 125\u2013169, 1984.","journal-title":"Acta Informatica"},{"key":"5146977_CR34","doi-asserted-by":"crossref","unstructured":"M.S. Papamarcos, J.H. Patel, \u201cA low-overhead coherence solution for multiprocessors with private cache memories,\u201d in Proceedings of 11th Annual Symposium on Computer Architecture (ISCA'84), Ann Arbor, USA, 1984, pp. 348\u2013354.","DOI":"10.1145\/800015.808204"},{"key":"5146977_CR35","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1016\/0304-3975(84)90029-X","volume":"32","author":"K. McAloon","year":"1984","unstructured":"K. McAloon, \u201cPetri nets and large finite sets,\u201d Theoretical Computer Science, Vol. 32, pp. 173\u2013183, 1984.","journal-title":"Theoretical Computer Science"},{"key":"5146977_CR36","unstructured":"K. McMillan, \u201cVerification of infinite state systems by compositional model checking,\u201d in L. Pierre and T. Kropf (Eds.), Proceedings of 10th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME\u2019 99), Lecture Notes in Computer Science, Bad Herrenalb, Germany, 1999, Vol. 1703, pp. 219\u2013234"},{"key":"5146977_CR37","unstructured":"K. McMillan and J. Schwalbe, \u201cVerification of infinite state systems by compositional model checking,\u201d in Proc. Int. Symp. on Shared Memory Multiprocessors, pp. 242\u2013251, 1991."},{"issue":"2","key":"5146977_CR38","doi-asserted-by":"crossref","first-page":"157","DOI":"10.1023\/A:1008678014487","volume":"11","author":"N. Halbwachs","year":"1997","unstructured":"N. Halbwachs, Y.-E. Proy, P. Raymond, \u201cVerification of real-time systems using linear relation analysis,\u201d Formal Methods in System Design, Vol. 11, No. 2, pp. 157\u2013185, 1997.","journal-title":"Formal Methods in System Design"},{"issue":"3","key":"5146977_CR39","doi-asserted-by":"crossref","first-page":"273","DOI":"10.1023\/A:1008723125149","volume":"14","author":"C. Norris Ip","year":"1999","unstructured":"C. Norris Ip and D.L. Dill, \u201cVerifying systems with replicated components in murphi,\u201d Formal Methods in System Design, Vol. 14, No. 3, pp. 273\u2013310, 1999.","journal-title":"Formal Methods in System Design"},{"key":"5146977_CR40","doi-asserted-by":"crossref","unstructured":"A. Pnueli, S. Ruah, and L.D. Zuck, \u201cAutomatic deductive verification with invisible invariants,\u201d in T. Margaria and W. Yi (Eds.), Proceedings of the 7th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS\u2019 01), Lecture Notes in Computer Science, Genova, Italy, 2001, Vol. 2031, pp. 82\u201397.","DOI":"10.1007\/3-540-45319-9_7"},{"key":"5146977_CR41","doi-asserted-by":"crossref","unstructured":"A. Pnueli and E. Shahar, \u201cLiveness and acceleration in parameterized verification,\u201d in E.A. Emerson and A.P. Sistla (Eds.), Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00), Lecture Notes in Computer Science, Chicago, Illinois, 2000, Vol. 1855, pp. 328\u2013343.","DOI":"10.1007\/10722167_26"},{"key":"5146977_CR42","doi-asserted-by":"crossref","unstructured":"F. Pong and M. Dubois, \u201cA new approach for the verification of cache coherence protocols,\u201d IEEE Transactions on Parallel and Distributed Systems, Vol. 6, No. 8, 1995.","DOI":"10.1109\/71.406955"},{"issue":"1","key":"5146977_CR43","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1145\/248621.248624","volume":"29","author":"F. Pong","year":"1997","unstructured":"F. Pong and M. Dubois, \u201cVerification techniques for cache coherence protocols,\u201d ACM Computing Surveys, Vol. 29, No. 1, pp. 82\u2013126, 1997.","journal-title":"ACM Computing Surveys"},{"key":"5146977_CR44","unstructured":"A. Schrijver, Theory of Linear and Integer Programming. Wiley-Interscience Series in Discrete Mathematics and Optimization. Wiley and Sons, 1998."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026276129010.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1026276129010\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1026276129010.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:24:04Z","timestamp":1754421844000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1026276129010"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,11]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,11]]}},"alternative-id":["5146977"],"URL":"https:\/\/doi.org\/10.1023\/a:1026276129010","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,11]]}}}