{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T03:21:28Z","timestamp":1778296888117,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540440437","type":"print"},{"value":"9783540456940","type":"electronic"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45694-5_8","type":"book-chapter","created":{"date-parts":[[2007,10,5]],"date-time":"2007-10-05T03:44:18Z","timestamp":1191555858000},"page":"101-115","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Network Invariants in Action*"],"prefix":"10.1007","author":[{"given":"Yonit","family":"Kesten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Elad","family":"Shahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,9,18]]},"reference":[{"issue":"2","key":"8_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, May 1991.","journal-title":"Theoretical Computer Science"},{"key":"8_CR2","doi-asserted-by":"crossref","unstructured":"K. R. Apt and D. Kozen. Limits for automatic program verification of finite-state concurrent systems. Information Processing Letters, 22(6), 1986.","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"8_CR3","unstructured":"M. Browne, E. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. PODC\u201986, pages 240\u2013248."},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. CONCUR\u201995, pages 395\u2013407.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"8_CR5","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0020-0190(83)90092-3","volume":"16","author":"E. Dijkstra","year":"1983","unstructured":"E. Dijkstra, W. Feijen, and A. van Gasteren. Derivation of a termination detection algorithm for disrtibued computations. Info. Proc. Lett., 16:217\u2013219, 1983.","journal-title":"Info. Proc. Lett."},{"key":"8_CR6","doi-asserted-by":"crossref","unstructured":"E. Emerson and V. Kahlon. Reducing model checking of the many to the few. In CADE-17, pages 236\u2013255, 2000.","DOI":"10.1007\/10721959_19"},{"key":"8_CR7","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201996","author":"E. Emerson","year":"1996","unstructured":"E. Emerson and K. Namjoshi. Automatic verification of parameterized synchronous systems. CAV\u201996, LNCS 1102."},{"key":"8_CR8","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1007\/BF01185559","volume":"29","author":"N. Halbwachs","year":"1992","unstructured":"N. Halbwachs, F. Lagnier, and C. Ratel. An experience in proving regular networks of processes by modular model checking. Acta Informatica, 29(6\/7):523\u2013543, 1992.","journal-title":"Acta Informatica"},{"key":"8_CR9","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201996","author":"C. Ip","year":"1996","unstructured":"C. Ip and D. Dill. Verifying systems with replicated components in Mur\u03c6. CAV\u201996, LNCS 1102."},{"issue":"4","key":"8_CR10","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"2","author":"Y. Kesten","year":"2000","unstructured":"Y. Kesten and A. Pnueli. Control and data abstractions: The cornerstones of formal verification. Software Tools for Technology Transfer, 2(4):328\u2013342, 2000.","journal-title":"Software Tools for Technology Transfer"},{"key":"8_CR11","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1006\/inco.2000.3000","volume":"163","author":"Y. Kesten","year":"2000","unstructured":"Y. Kesten and A. Pnueli. Verification by augmented finitary abstraction. Information and Computation, a special issue on Compositionality, 163:203\u2013243, 2000.","journal-title":"Information and Computation, a special issue on Compositionality"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Y. Kesten, A. Pnueli, E. Shahar, and L. D. Zuck. Network invariant in action. Technical report, The weizmann Institute of Science, 2002.","DOI":"10.1007\/3-540-45694-5_8"},{"key":"8_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1995.1024","volume":"117","author":"R. P. Kurshan","year":"1995","unstructured":"R. P. Kurshan and K. L. McMillan. A structural induction theorem for processes. Information and Computation, 117:1\u201311, 1995.","journal-title":"Information and Computation"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"D. Lehmann and M. O. Rabin. On the advantages of free choice: A symmetric and fully distributed solution to the dining philosophers problem. POPL\u201981, pages 133\u2013138.","DOI":"10.1145\/567532.567547"},{"key":"8_CR15","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. POPL\u201997."},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00f8rner, A. Browne, E. Chang, M. Col\u00f3n, L. D. Alfaro, H. Devarajan, H. Sipma, and T. Uribe. STeP: The Stanford Temporal Prover. Stanford, California, 1994.","DOI":"10.21236\/ADA324036"},{"key":"8_CR17","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Verlag, New York, 1991."},{"key":"8_CR18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"8_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1007\/3-540-45319-9_7","volume-title":"TACAS\u201901","author":"A. Pnueli","year":"2001","unstructured":"A. Pnueli, S. Ruah, and L. Zuck. Automatic deductive verification with invisible invariants. TACAS\u201901, LNCS 2031, pages 82\u201397."},{"key":"8_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/3-540-61474-5_68","volume-title":"CAV\u201996","author":"A. Pnueli","year":"1996","unstructured":"A. Pnueli and E. Shahar. A platform for combining deductive with algorithmic verification. CAV\u201996, LNCS 1102, pages 184\u2013195."},{"key":"8_CR21","unstructured":"A. Pnueli, J. Xu, and L. Zuck. Liveness with (0, 1,\u221e)-counter abstraction. To appear in CAV\u201902."},{"key":"8_CR22","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201901","author":"A. Roychoudhury","year":"2001","unstructured":"A. Roychoudhury and I. Ramakrishnan. Automated inductive verification of parameterized protocols. CAV\u201901, LNCS 2102."},{"key":"8_CR23","series-title":"Lect Notes Comput Sci","first-page":"151","volume-title":"CAV\u201989","author":"Z. Shtadler","year":"1989","unstructured":"Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. CAV\u201989, LNCS 407, pages 151\u2013165."},{"key":"8_CR24","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"A. Sistla","year":"1992","unstructured":"A. Sistla and S. German. Reasoning about systems with many processes. J. ACM, 39:675\u2013735, 1992.","journal-title":"J. ACM"},{"key":"8_CR25","series-title":"Lect Notes Comput Sci","first-page":"68","volume-title":"CAV\u201989","author":"P. Wolper","year":"1989","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. CAV\u201989, LNCS 407, pages 68\u201380."},{"key":"8_CR26","series-title":"Lect Notes Comput Sci","volume-title":"Automatic verification of free choice","author":"L. Zuck","year":"2002","unstructured":"L. Zuck, A. Pnueli, and Y. Kesten. Automatic verification of free choice. In Proc. of the 3rd workshop on Verification, Model Checking, and Abstract Interpretation, LNCS 2294, 2002."}],"container-title":["Lecture Notes in Computer Science","CONCUR 2002 \u2014 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45694-5_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,8]],"date-time":"2026-05-08T13:45:17Z","timestamp":1778247917000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/3-540-45694-5_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540440437","9783540456940"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-45694-5_8","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]},"assertion":[{"value":"18 September 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}