{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T10:48:29Z","timestamp":1742381309964,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540648277"},{"type":"electronic","value":"9783540685326"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055757","type":"book-chapter","created":{"date-parts":[[2006,8,17]],"date-time":"2006-08-17T17:36:31Z","timestamp":1155836191000},"page":"54-71","source":"Crossref","is-referenced-by-count":12,"title":["Modularization and abstraction: The keys to practical formal verification"],"prefix":"10.1007","author":[{"given":"Yonit","family":"Kesten","sequence":"first","affiliation":[]},{"given":"Amir","family":"Pnueli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,5,28]]},"reference":[{"key":"4_CR1","first-page":"251","volume":"663","author":"S. Bensalem","year":"1992","unstructured":"S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Properties preserving simulations. CAV'92, vol. 663 of LNCS, pp 251\u2013263, 1992.","journal-title":"LNCS"},{"key":"4_CR2","first-page":"589","volume":"976","author":"N. Bj\u00d8rner","year":"1995","unstructured":"N. Bj\u00d8rner, I.A. Browne, and Z. Manna. Automatic generation of invariants and intermediate assertions. 1st Intl. Conf. on Principles and Practice of Constraint Programming, vol. 976 of LNCS, pp 589\u2013623, 1995.","journal-title":"LNCS"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"M.C. Browne, E.M. Clarke, and O. Grumberg. Reasoning about networks with many finite state processes. PODC'86, pp 240\u2013248, 1986.","DOI":"10.1145\/10590.10611"},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. POPL'77, 1977.","DOI":"10.1145\/512950.512973"},{"key":"4_CR5","first-page":"415","volume":"818","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, and K. Hamaguchi. Another look at Ltl model checking. CAV'94, vol. 818 of LNCS, pp 415\u2013427, 1994.","journal-title":"LNCS"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and S. Jha. Verifying parametrized networks using abstraction and regular languages. CONCUR'95, pp 395\u2013407, 1995.","DOI":"10.1007\/3-540-60218-6_30"},{"issue":"5","key":"4_CR7","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Trans. Prog. Lang. Sys., 16(5):1512\u20131542, 1994.","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking. Model Checking, Abstraction and Composition, vol. 152 of Nato ASI Series F, pages 477\u2013498. Springer-Verlag, 1996.","DOI":"10.1007\/978-3-642-61455-2_16"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"P. Cousot and N. Halbwachs. Automatic discovery of linear restraints among variables of a program. POPL'78, pp 84\u201396, 1978.","DOI":"10.1145\/512760.512770"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Abstract interpretation of reactive systems. ACM Trans. Prog. Lang. Sys., 19(2), 1997.","DOI":"10.1145\/244795.244800"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"E. A. Emerson and K. S. Namjoshi. Reasoning about rings. POPL'95, 1995.","DOI":"10.1145\/199448.199468"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"E.A. Emerson and K.S. Namjoshi. Automatic verification of parameterized synchronous systems. CAV'96, LNCS, 1996.","DOI":"10.1007\/3-540-61474-5_60"},{"key":"4_CR13","first-page":"71","volume":"697","author":"S. Graf","year":"1993","unstructured":"S. Graf and C. Loiseaux. A tool for symbolic program verification and abstraction. CAV'93, vol. 697 of LNCS, pp 71\u201384, 1993.","journal-title":"LNCS"},{"issue":"6\/7","key":"4_CR14","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":"4_CR15","unstructured":"C.N. Ip and D. Dill. Verifying systems with replicated components in Mur\u03d5. CAV'96, LNCS, 1996."},{"key":"4_CR16","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":"4_CR17","doi-asserted-by":"crossref","unstructured":"Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic verification of linear temporal logic specifications. ICALP'98, LNCS, 1998.","DOI":"10.1007\/BFb0055036"},{"key":"4_CR18","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L. Lamport","year":"1977","unstructured":"L. Lamport. Proving the correctness of multiprocess programs. IEEE Trans. Software Engin., 3:125\u2013143, 1977.","journal-title":"IEEE Trans. Software Engin."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"D. Lesens, N. Halbwachs, and P. Raymond. Automatic verification of parameterized linear networks of processes. POPL'97, 1997.","DOI":"10.1145\/263699.263747"},{"key":"4_CR20","first-page":"264","volume":"115","author":"D. Lehmann","year":"1981","unstructured":"D. Lehmann, A. Pnueli, and J. Stavi. Impartiality, justice and fairness: The ethics of concurrent termination. ICALP'81, vol. 115 of LNCS, pp 264\u2013277, 1981.","journal-title":"LNCS"},{"key":"4_CR21","volume-title":"Technical Report STAN-CS-TR-94-1518","author":"Z. Manna","year":"1994","unstructured":"Z. Manna, A. Anuchitanukul, N. Bj\u00d8rner, 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":"4_CR22","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":"4_CR23","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":"4_CR24","first-page":"151","volume":"407","author":"Z. Shtadler","year":"1989","unstructured":"Z. Shtadler and O. Grumberg. Network grammars, communication behaviors and automatic verification. CAV'89, vol. 407 of LNCS, pp 151\u2013165, 1989.","journal-title":"LNCS"},{"key":"4_CR25","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":"4_CR26","first-page":"68","volume":"407","author":"P. Wolper","year":"1989","unstructured":"P. Wolper and V. Lovinfosse. Verifying properties of large sets of processes with network invariants. CAV'89, vol. 407 of LNCS, pp 68\u201380, 1989.","journal-title":"LNCS"}],"container-title":["Lecture Notes in Computer Science","Mathematical Foundations of Computer Science 1998"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055757","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T13:52:07Z","timestamp":1736517127000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055757"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540648277","9783540685326"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/bfb0055757","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}