{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:50:29Z","timestamp":1770285029115,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540418658","type":"print"},{"value":"9783540453192","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45319-9_7","type":"book-chapter","created":{"date-parts":[[2007,7,16]],"date-time":"2007-07-16T15:50:47Z","timestamp":1184601047000},"page":"82-97","source":"Crossref","is-referenced-by-count":133,"title":["Automatic Deductive Verification with Invisible Invariants"],"prefix":"10.1007","author":[{"given":"Amir","family":"Pnueli","sequence":"first","affiliation":[]},{"given":"Sitvanit","family":"Ruah","sequence":"additional","affiliation":[]},{"given":"Lenore","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"7_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-48683-6_14","volume-title":"CAV\u201999","author":"P.A. Abdulla","year":"1999","unstructured":"P.A. Abdulla, A. Bouajjani, B. Jonsson, and M. Nilsson. Handling global conditions in parametrized system verification. In CAV\u201999, LNCS 1633, pages 134\u2013145, 1999."},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"K. R. Apt and D. Kozen. Limits for automatic program verification of finitestate concurrent systems. Information Processing Letters, 22(6), 1986.","DOI":"10.1016\/0020-0190(86)90071-2"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. In Proc. 5th ACM Symp. Princ. of Dist. Comp., pages 240\u2013248, 1986.","DOI":"10.1145\/10590.10611"},{"issue":"1\/2","key":"7_CR4","first-page":"8","volume":"9","author":"E.M. Clarke","year":"1996","unstructured":"E.M. Clarke, R. Enders, T. Filkron, and S. Jha. Exploiting symmetry in temporal logic model checking. Formal Methods in System Design, 9(1\/2), 8 1996. Preliminary version appeared in 5th CAV, 1993.","journal-title":"Formal Methods in System Design"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. In 6th International Conference on Concurrency Theory (CONCUR\u201995), pages 395\u2013407, Philadelphia, PA, August 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"key":"7_CR6","unstructured":"S.J. Creese and A.W. Roscoe. Formal verification of arbitrary network topologies. In Proc. of the Int. Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA\u201999), Las Vegas, 1999. CSREA Press."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"S.J. Creese and A.W. Roscoe. Verifying an infinite family of inductions simultaneously using data independence and fdr. In Formal Description Techniques for Distributed Systems and Communication Protocols and Protocol Specification, Testing and Verification (FORTE\/PSTV\u201999), Beijing, 1999. Kluwer Academic Publishers.","DOI":"10.1007\/978-0-387-35578-8_25"},{"key":"7_CR8","unstructured":"S.J. Creese and A.W. Roscoe. Data independent induction over structured networks. In Proc. of the Int. Conf. on Parallel and Distributed Processing Techniques and Applications (PDPTA\u201900), Las Vegas, June 2000. CSREA Press."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and V. Kahlon. Reducing model checking of the many to the few. In 17th International Conference on Automated Deduction (CADE-17), pages 236\u2013255, 2000.","DOI":"10.1007\/10721959_19"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Reasoning about rings. In POPL\u201995, 1995.","DOI":"10.1145\/199448.199468"},{"key":"7_CR11","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201996","author":"E.A. Emerson","year":"1996","unstructured":"E.A. Emerson and K.S. Namjoshi. Automatic verification of parameterized synchronous systems. In CAV\u201996, LNCS 1102, 1996."},{"issue":"1\/2","key":"7_CR12","first-page":"8","volume":"9","author":"E. A. Emerson","year":"1996","unstructured":"E. A. Emerson and A. P. Sistla. Symmetry and model checking. Formal Methods in System Design, 9(1\/2), 8 1996. Preliminary version appeared in 5th CAV, 1993.","journal-title":"Formal Methods in System Design"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and A. P. Sistla. Utilizing symmetry when model checking under fairness assumptions. ACM Trans. Prog. Lang. Sys., 19(4), 1997. Preliminary version appeared in 7th CAV, 1995.","DOI":"10.1145\/262004.262008"},{"key":"7_CR14","unstructured":"Ger00. S. German. Personal Communication, 2000."},{"key":"7_CR15","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201997","author":"V. Gyuris","year":"1997","unstructured":"V. Gyuris and A. P. Sistla. On-the-y model checking under fairness that exploits symmetry. In CAV\u201997, LNCS 1254, 1997."},{"key":"7_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"424","DOI":"10.1007\/BFb0054187","volume-title":"TACAS\u201998","author":"E.P. Gribomont","year":"1998","unstructured":"E.P. Gribomont and G. Zenner. Automated verification of szymanski\u2019s algorithm. In TACAS\u201998, LNCS 1384, pages 424\u2013438, 1998."},{"issue":"6\/7","key":"7_CR17","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":"7_CR18","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201996","author":"C.N. Ip","year":"1996","unstructured":"C.N. Ip and D. Dill. Verifying systems with replicated components in Mur\u03d5 In CAV\u201996, LNCS 1102, 1996."},{"key":"7_CR19","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"409","DOI":"10.1007\/BFb0054186","volume-title":"TACAS\u201998","author":"E. Jensen","year":"1998","unstructured":"E. Jensen and N.A. Lynch. A proof of burn\u2019s n-process mutual exclusion algorithm using abstraction. In TACAS\u201998, LNCS 1384, pages 409\u2013423, 1998."},{"key":"7_CR20","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201900","author":"B. Jonsson","year":"2000","unstructured":"B. Jonsson and M. Nilsson. Transitive closures of regular relations for verifying infinite-state systems. In TACAS\u201900, LNCS 1785, 2000."},{"key":"7_CR21","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":"7_CR22","series-title":"Lect Notes Comput Sci","first-page":"424","volume-title":"CAV\u201997","author":"Y. Kesten","year":"1997","unstructured":"Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolic model checking with rich assertional languages. In CAV\u201997, LNCS 1254, pages 424\u2013435, 1997."},{"issue":"2","key":"7_CR23","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/s100090050040","volume":"4","author":"Y. Kesten","year":"2000","unstructured":"Y. Kesten and A. Pnueli. Control and data abstractions: The cornerstones of practical formal verification. Software Tools for Technology Transfer, 4(2):328\u2013342, 2000.","journal-title":"Software Tools for Technology Transfer"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. In POPL\u201997, 1997.","DOI":"10.1145\/263699.263747"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"D. Lesens and H. Saidi. Automatic verification of parameterized networks of processes by abstraction. In 2nd International Workshop on the Verification of Infinite State Systems (INFINITY\u201997), 1997.","DOI":"10.1145\/263699.263747"},{"key":"7_CR26","series-title":"Technical Report","doi-asserted-by":"crossref","DOI":"10.21236\/ADA324036","volume-title":"STeP: The Stanford Temporal Prover","author":"Z. Manna","year":"1994","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00e5rner, A. Browne, E. Chang, M. Col\u00f3n, L. De Alfaro, H. Devarajan, H. Sipma, and T.E. Uribe. STeP: The Stanford Temporal Prover. Technical Report STAN-CS-TR-94-1518, Dept. of Comp. Sci., Stanford University, Stanford, California, 1994."},{"key":"7_CR27","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"CAV\u201998","author":"K.L. McMillan","year":"1998","unstructured":"K.L. McMillan. Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In CAV\u201998, LNCS 1427, pages 110\u2013121, 1998."},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli. An exercise in the verification of multiprocess programs. In W.H.J. Feijen, A.J.M van Gasteren, D. Gries, and J. Misra, editors, Beauty is Our Business, pages 289\u2013301. Springer-Verlag, 1990.","DOI":"10.1007\/978-1-4612-4476-9_34"},{"key":"7_CR29","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u201900","author":"A. Pnueli","year":"2000","unstructured":"A. Pnueli and E. Shahar. Livenss and acceleraiton in parameterized verification. In CAV\u201900, LNCS 1855, 2000."},{"key":"7_CR30","series-title":"Lect Notes Comput Sci","volume-title":"TACAS\u201900","author":"A. Roychoudhury","year":"2000","unstructured":"A. Roychoudhury, K. Narayan Kumar, C. R. Ramakrishnan, I.V. Ramakrishnan, and S.A. Smolka. Verification of parameterized systems using logic program transformations. In TACAS\u201900, LNCS 1785, 2000."},{"key":"7_CR31","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. In CAV\u201989, LNCS 407, pages 151\u2013165, 1989."},{"key":"7_CR32","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"A.P. Sistla","year":"1992","unstructured":"A.P. Sistla and S.M. German. Reasoning about systems with many processes. J. ACM, 39:675\u2013735, 1992.","journal-title":"J. ACM"},{"key":"7_CR33","series-title":"Technical report","volume-title":"The PVS proof checker: A reference manual (draft)","author":"N. Shankar","year":"1993","unstructured":"N. Shankar, S. Owre, and J.M. Rushby. The PVS proof checker: A reference manual (draft). Technical report, Comp. Sci.,Laboratory, SRI International, Menlo Park, CA, 1993."},{"key":"7_CR34","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. In CAV\u201989, LNCS 407, pages 68\u201380, 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-45319-9_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,19]],"date-time":"2025-01-19T11:41:10Z","timestamp":1737286870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45319-9_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418658","9783540453192"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/3-540-45319-9_7","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2001]]}}}