{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:26:45Z","timestamp":1761611205909,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_22","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"295-308","source":"Crossref","is-referenced-by-count":4,"title":["Algorithmic Verification of Invalidation-Based Protocols"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bozzano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Giorgio","family":"Delzanno","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, K. Cer\u0101ns, B. Jonsson, Y.-K. Tsay. General Decidability Theorems for Infinite-State Systems. In Proc. LICS\u201996, pp. 313\u2013321, 1996.","DOI":"10.1109\/LICS.1996.561359"},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, B. Jonsson. Verifying Networks of Timed Processes (Extended Abstract). In Proc. TACAS\u2019 98, pp. 298\u2013312. Springer, 1998.","DOI":"10.1007\/BFb0054179"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, B. Jonsson. Channel Representations in Protocol Verification. In Proc. CONCUR 2001, pp. 1\u201315. Springer, 2001.","DOI":"10.1007\/3-540-44685-0_1"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"P. A. Abdulla, A. Nyl\u00e9n. Better is Better than Well: On Efficient Verification of Infinite-State Systems. In Proc. LICS 2000, pp. 132\u2013140, 2000.","DOI":"10.1109\/LICS.2000.855762"},{"issue":"4","key":"22_CR5","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1145\/6513.6514","volume":"4","author":"P. A. Archibald","year":"1986","unstructured":"P. A. Archibald, J. Baer. Cache Coherence Protocols: Evaluation Using a Multiprocessor Simulation Model. TOCS 4(4): 273\u2013298. 1986.","journal-title":"TOCS"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"T. Arons, A. Pnueli, S. Ruah, Y. Xu, L. Zuck Parameterized Verification with Automatically Computed Inductive Assertions. In Proc. CAV\u2019 01, pp. 221\u2013234, 2001.","DOI":"10.1007\/3-540-44585-4_19"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"K. Baukus, S. Bensalem, Y. Lakhnech, K. Stahl. Abstracting WS1S Systems to Verify Parameterized Networks. In Proc. TACAS\u2019 00, pp. 188\u2013203, 2000.","DOI":"10.1007\/3-540-46419-0_14"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"K. Baukus, K. Stahl, S. Bensalem, Y. Lakhnech. Networks of Processes with Parameterized State Space. In Proc. VEPAS\u2019 01, ENTCS vol. 50, issue 4, 2001.","DOI":"10.1016\/S1571-0661(04)00190-2"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, B. Jonsson, M. Nilsson, T. Touilli. Regular Model Checking. In Proc. CAV\u201900, pp. 403\u2013418, 2000.","DOI":"10.1007\/10722167_31"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"M. Bozzano, G. Delzanno. Beyond Parameterized Verification. In Proc. TACAS\u201902, April 2002.","DOI":"10.1007\/3-540-46002-0_16"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"I. Cervesato, N. A. Durgin, P. Lincoln, J. C. Mitchell, A. Scedrov. A Meta-notation for Protocol Analysis. In Proc. CSFW 1999, pp. 55\u201369, 1999.","DOI":"10.1109\/CSFW.1999.779762"},{"issue":"5","key":"22_CR12","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1145\/265943.265960","volume":"19","author":"E. Clarke","year":"1997","unstructured":"E. Clarke, O. Grumberg, S. Jha. Verifying Parameterized Networks. TOPLAS 19(5): 726\u2013750, 1997.","journal-title":"TOPLAS"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"G. Delzanno. Automatic Verification of Parameterized Cache Coherence Protocols. In Proc. CAV 2000, pp. 53\u201368, 2000.","DOI":"10.1007\/10722167_8"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"G. Delzanno. An assertional language for systems parametric in several dimensions. In Proc. VEPAS 2001, ENTCS 50(4), 2001.","DOI":"10.1016\/S1571-0661(04)00189-6"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"E. A. Emerson, K. S. Namjoshi. On Model Checking for Non-deterministic Infinite-state Systems. In Proc. LICS\u2019 98, pp. 70\u201380, 1998.","DOI":"10.1109\/LICS.1998.705644"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"J. Esparza, A. Finkel, R. Mayr. On the Verification of Broadcast Protocols. In Proc. LICS\u201999, pp. 352\u2013359, 1999.","DOI":"10.1109\/LICS.1999.782630"},{"issue":"1\u20132","key":"22_CR17","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"A. Finkel, P. Schnoebelen. Well-structured transition systems everywhere! TCS, 256(1\u20132):63\u201392, 2001.","journal-title":"TCS"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"K. Fisler, C. Girault. Modelling and Model Checking a Distributed Shared Memory Consistency Protocol. In Proc. ICATPN\u2019 98, pp. 84\u2013103, 2001.","DOI":"10.1007\/3-540-69108-1_6"},{"key":"22_CR19","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"2","author":"G. Highman","year":"1952","unstructured":"G. Highman. Ordering by Divisibility in Abstract Algebras. Proc. London Math. Soc., 2:326\u2013336, 1952.","journal-title":"Proc. London Math. Soc."},{"issue":"4","key":"22_CR20","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1145\/75104.75105","volume":"7","author":"K. Li","year":"1989","unstructured":"K. Li, P. Hudak. Memory Coherence in Shared Virtual Memory Systems. TOCS 7(4): 321\u2013359, 1989.","journal-title":"TOCS"},{"key":"22_CR21","doi-asserted-by":"crossref","unstructured":"D. Mentr\u00e9, D. Le M\u00e9tayer, T. Priol. Formalization and Verification of Coherence Protocols with the Gamma Framework. In Proc. PDSE 2000, pp. 105\u2013113, 2000.","DOI":"10.1109\/PDSE.2000.847855"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, E. Shahar. Symbolic Model Checking with Rich Assertional Languages. In Proc. CAV\u201997, pp. 424\u2013435, 1997.","DOI":"10.1007\/3-540-63166-6_41"},{"issue":"4","key":"22_CR23","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/s001650050040","volume":"11","author":"A. P. Sistla","year":"1999","unstructured":"A. P. Sistla, V. Gyuris. Parametrized Verification of Linear Networks using Automata as Invariants. Formal Aspects of Computing, 11(4):402\u2013425, 1999.","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,16]],"date-time":"2025-01-16T13:10:54Z","timestamp":1737033054000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_22","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}