{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,20]],"date-time":"2025-02-20T05:19:07Z","timestamp":1740028747364,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540008989"},{"type":"electronic","value":"9783540365778"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/3-540-36577-x_11","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T21:12:04Z","timestamp":1269897124000},"page":"144-159","source":"Crossref","is-referenced-by-count":17,"title":["Rapid Parameterized Model Checking of Snoopy Cache Coherence Protocols"],"prefix":"10.1007","author":[{"given":"E. Allen","family":"Emerson","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vineet","family":"Kahlon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2003,2,28]]},"reference":[{"key":"11_CR1","doi-asserted-by":"crossref","unstructured":"P. Abdulla, K. Cerans, B. Jonsson, Y. K. Tsay. General Decidability Theorems for Infinite State Systems. LICS. 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"P. Abdulla, A. Boujjani, B. Jonsson and M. Nilsson. Handling global conditions in parameterized systems verification. CAV 1999.","DOI":"10.1007\/3-540-48683-6_14"},{"key":"11_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"180","DOI":"10.1007\/3-540-48092-7_9","volume-title":"Correct System Design-Recent Insights and Advances","author":"P. Abdulla","year":"1999","unstructured":"P. Abdulla and B. Jonsson. On the existence of network invariants for verifying parameterized systems. In Correct System Design-Recent Insights and Advances, 1710, LNCS, pp 180\u2013197, 1999."},{"key":"11_CR4","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1016\/0020-0190(86)90071-2","volume":"15","author":"K. Apt","year":"1986","unstructured":"K. Apt and D. Kozen. Limits for automatic verification of finite-state concurrent systems. Information Processing Letters, 15, pages 307\u2013309, 1986.","journal-title":"Information Processing Letters"},{"key":"11_CR5","series-title":"Lect Notes Comput Sci","volume-title":"CAV 2001","author":"T. Arons","year":"2001","unstructured":"T. Arons, A. Pnueli, S. Ruah, J, Xu and L. Zuck. ParameterizedVerification withAutomatically Computed Inductive Assertions. CAV 2001, LNCS 2102, 2001."},{"issue":"1","key":"11_CR6","first-page":"13","volume":"81","author":"M.C. Browne","year":"1989","unstructured":"M.C. Browne, E.M. Clarke and O. Grumberg. Reasoning about Networks with Many Identical Finite State Processes. Information and Control, 81(1), pages 13\u201331, April 1989.","journal-title":"Information and Control"},{"key":"11_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"395","DOI":"10.1007\/3-540-60218-6_30","volume-title":"CONCUR","author":"E.M. Clarke","year":"1995","unstructured":"E.M. Clarke, O. Grumberg and S. Jha. Verifying Parameterized Networks using Abstraction and Regular Languages. CONCUR. LNCS 962, pages 395\u2013407, Springer-Verlag, 1995."},{"key":"11_CR8","unstructured":"D. E. Culler and J. P. Singh. Parallel Computer Architecture:A Hardware\/Software Approach. Morgan Kaufmann Publishers, 1998."},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. CAV 2000, 51\u201368.","DOI":"10.1007\/10722167_8"},{"key":"11_CR10","unstructured":"E.A. Emerson and V. Kahlon. This paper, full version. Available at http:\/\/www.cs.utexas.edu\/users\/{emerson,kahlon}\/tacas03\/"},{"key":"11_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/10722167","volume-title":"CADE-17","author":"E.A. Emerson","year":"2000","unstructured":"E.A. Emerson and V. Kahlon. Reducing Model Checking of the Many to the Few. CADE-17. LNCS, Springer-Verlag, 2000."},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and V. Kahlon. Model Checking Large-Scale and Parameterized Resource Allocation Systems. TACAS, 2002.","DOI":"10.1007\/3-540-46002-0_18"},{"key":"11_CR13","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. Reasoning about Rings. POPL. pages 85\u201394, 1995.","DOI":"10.1145\/199448.199468"},{"key":"11_CR14","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. On Model Checking for Non-Deterministic Infinite-State Systems. LICS 1998.","DOI":"10.1109\/LICS.1998.705644"},{"key":"11_CR15","series-title":"Lect Notes Comput Sci","volume-title":"CAV","author":"E.A. Emerson","year":"1996","unstructured":"E.A. Emerson and K.S. Namjoshi. Automatic Verification of Parameterized Synchronous Systems. CAV. LNCS, Springer-Verlag, 1996."},{"key":"11_CR16","doi-asserted-by":"crossref","unstructured":"J. Esparza, A Finkel and R. Mayr, On the Verification of Broadcast Protocols. LICS 1999.","DOI":"10.1109\/LICS.1999.782630"},{"key":"11_CR17","unstructured":"A. Finkel and J. Leroux. A finite covering tree for analyzing entropic broadcast protocols. Proc. VCL 2000. Report DSSE-TR-2000-6, Univ. Southampton, GB."},{"key":"11_CR18","doi-asserted-by":"crossref","unstructured":"S.M. German and A.P. Sistla. Reasoning about Systems with Many Processes. J. ACM, 39(3), July 1992.","DOI":"10.1145\/146637.146681"},{"key":"11_CR19","unstructured":"J. Handy. The Cache Memory Book. Academic Press, 1993."},{"key":"11_CR20","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and K. L. McMillan. A Structural Induction Theorem for Processes. PODC. pages 239\u2013247, 1989.","DOI":"10.1145\/72981.72998"},{"key":"11_CR21","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs and P. Raymond. Automatic Verification of Parameterized Linear Network of Processes. POPL 1997. pp 346\u2013357, 1997. Parallel Coordination Programs I.Acta Informatica 21, 1984.","DOI":"10.1145\/263699.263747"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"M. Maidl. A Unifying Model Checking Approach for Safety Properties of Parameterized Systems. CAV 2001.","DOI":"10.1007\/3-540-44585-4_29"},{"key":"11_CR23","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1016\/0304-3975(84)90029-X","volume":"32","author":"K. McAloon","year":"1984","unstructured":"K. McAloon. Petri Nets and Large Finite Sets. Theoretical Computer Science 32, pp. 173\u2013183, 1984.","journal-title":"Theoretical Computer Science"},{"key":"11_CR24","series-title":"Lect Notes Comput Sci","volume-title":"TACAS 2001","author":"A. Pnueli","year":"2001","unstructured":"A. Pnueli, S. Ruah and L. Zuck. Automatic Deductive Verification with Invisible Invariants. TACAS 2001, LNCS, 2001."},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"F. Pong and M. Dubois. A NewApproach for theVerification of Cache Coherence Protocols. IEEE Transactions on Parallel and Distributed Systems, Vol. 6, No. 8, August 1995.","DOI":"10.1109\/71.406955"},{"key":"11_CR26","unstructured":"A. P. Sistla, Parameterized Verification of Linear Networks Using Automata as Invariants, CAV, 5."},{"key":"11_CR27","series-title":"Lect Notes Comput Sci","volume-title":"AutomaticVerification Methods for Finite State Systems","author":"P. Wolper","year":"1989","unstructured":"P. Wolper and V. Lovinfosse. Verifying Properties of Large Sets of Processes with Network Invariants. In J. Sifakis(ed) AutomaticVerification Methods for Finite State Systems, Springer-Verlag, LNCS 407, 1989."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-36577-X_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,19]],"date-time":"2025-02-19T19:10:34Z","timestamp":1739992234000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-36577-X_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540008989","9783540365778"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-36577-x_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2003]]}}}