{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:08:27Z","timestamp":1754482107816},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581796"},{"type":"electronic","value":"9783540484691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_58","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:25:09Z","timestamp":1330269909000},"page":"234-246","source":"Crossref","is-referenced-by-count":5,"title":["On the automatic computation of network invariants"],"prefix":"10.1007","author":[{"given":"Felice","family":"Balarin","sequence":"first","affiliation":[]},{"given":"Alberto L.","family":"Sangiovanni-Vincentelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Felice Balarin and Alberto L. Sangiovanni-Vincentelli. On the automatic computation of network invariants, 1994. UCB\/ERL M94\/18.","key":"20_CR1","DOI":"10.1007\/3-540-58179-0_58"},{"issue":"1","key":"20_CR2","doi-asserted-by":"publisher","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. Reasoning about networks with many identical finite state processes. Information and Computation, 81(1):13\u201331, 1989.","journal-title":"Information and Computation"},{"unstructured":"E. M. Clarke, O. Grumberg, H. Hiraisi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Futurebus+ cache coherence protocol. In Proc. 11th Intl. Symp. on Comput. Hardware Description Lang, and their Applications, 1993.","key":"20_CR3"},{"doi-asserted-by":"crossref","unstructured":"Frederick C. Hennie. Iterative Arrays of Logical Circuits. MIT Press and John Eiley Sons, Inc., 1961.","key":"20_CR4","DOI":"10.7551\/mitpress\/3999.001.0001"},{"doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and K. L. McMillan. A structural induction theorem for processes. In Proceedings of the 8th ACM Symp. PODC, 1989.","key":"20_CR5","DOI":"10.1145\/72981.72998"},{"doi-asserted-by":"crossref","unstructured":"J.K. Rho and F. Somenzi. Inductive verification of iterative systems. In Proceedings of the 29th ACM\/IEEE Design Automation Conference, pages 628\u201333, June 1992.","key":"20_CR6","DOI":"10.1109\/DAC.1992.227809"},{"key":"20_CR7","first-page":"123","volume-title":"LNCS vol. 697","author":"J.K. Rho","year":"1993","unstructured":"J.K. Rho and F. Somenzi. Automatic generation of network invariants for the verification of iterative sequential systems. In Costas Courcoubetis, editor, Computer Aided Verification: 5th International Conference, CAV'93, Elounda, Greece, June\/July 1993, Proceedings, pages 123\u2013137. Springer-Verlag, 1993. LNCS vol. 697."},{"key":"20_CR8","first-page":"151","volume-title":"LNCS vol. 407","author":"Z. Shtadler","year":"1990","unstructured":"Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, International Workshop Proceedings, Grenoble, France, 12\u201314 June 1989, pages 151\u201365. Springer-Verlag, 1990. LNCS vol. 407."},{"key":"20_CR9","first-page":"68","volume-title":"LNCS vol. 407","author":"P. Wolper","year":"1990","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems, International Workshop Proceedings, Grenoble, France, 12\u201314 June 1989, pages 68\u201380. Springer-Verlag, 1990. LNCS vol. 407."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_58.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:55Z","timestamp":1605647875000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}