{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T15:26:14Z","timestamp":1759332374902},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540677703"},{"type":"electronic","value":"9783540450474"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/10722167_14","type":"book-chapter","created":{"date-parts":[[2006,12,29]],"date-time":"2006-12-29T22:00:33Z","timestamp":1167429633000},"page":"139-153","source":"Crossref","is-referenced-by-count":30,"title":["On the Completeness of Compositional Reasoning"],"prefix":"10.1007","author":[{"given":"Kedar S.","family":"Namjoshi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Richard J.","family":"Trefler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.: Reactive modules. In: IEEE LICS (1996)","DOI":"10.1109\/LICS.1996.561320"},{"key":"14_CR2","doi-asserted-by":"crossref","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. on Programming Languages and Systems, TOPLAS (May 1995)","DOI":"10.1145\/203095.201069"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131. Springer, Heidelberg (1982)","DOI":"10.1007\/BFb0025774"},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic. ACM Transactions on Programming Languages and Systems (TOPLAS)\u00a08(2) (1986)","DOI":"10.1145\/5397.5399"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: IEEE LICS (1989)","DOI":"10.1109\/LICS.1989.39190"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Proofs of networks of processes. IEEE Transactions on Software Engineering\u00a07(4) (1981)","DOI":"10.1109\/TSE.1981.230844"},{"key":"14_CR7","unstructured":"de Roever, W.-P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Draft book (1999)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","volume-title":"Compositionality: The Significant Difference","year":"1998","unstructured":"de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.): COMPOS 1997. LNCS, vol.\u00a01536. Springer, Heidelberg (1998)"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Gr\u00fcmberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. on Programming Languages and Systems, TOPLAS (1994)","DOI":"10.1145\/177492.177725"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM (1969)","DOI":"10.1145\/363235.363259"},{"key":"14_CR11","series-title":"NATO Advanced Summer Institutes","doi-asserted-by":"crossref","first-page":"477","DOI":"10.1007\/978-3-642-82453-1_17","volume-title":"Logics and Models of Concurrent Systems","author":"D. Harel","year":"1985","unstructured":"Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K. (ed.) Logics and Models of Concurrent Systems. NATO Advanced Summer Institutes, vol.\u00a0F-13, pp. 477\u2013498. Springer, Heidelberg (1985)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/3-540-49519-3_27","volume-title":"Formal Methods in Computer-Aided Design","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Qadeer, S., Rajamani, S.K., Ta\u015f\u0131ran, S.: An assume-guarantee rule for checking simulation. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 421\u2013431. Springer, Heidelberg (1998)"},{"key":"14_CR13","unstructured":"Jones, C.B.: Development methods for computer programs including a notion of interference. PhD thesis, Oxford University (1981)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Josko, B.: Model checking of CTL formulae under liveness assumptions. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol.\u00a0267. Springer, Heidelberg (1987)","DOI":"10.1007\/3-540-18088-5_23"},{"key":"14_CR15","series-title":"Lecture Notes in Computer Science","volume-title":"Directions in Human Factors for Interactive Systems","author":"R.P. Kurshan","year":"1981","unstructured":"Kurshan, R.P.: Reducibility in analysis of coordination. In: Ledgard, H., Whiteside, J., Singer, A. (eds.) Directions in Human Factors for Interactive Systems. LNCS, vol.\u00a0103, Springer, Heidelberg (1981)"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: On the complexity of branching modular model checking. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol.\u00a0962. Springer, Heidelberg (1995)","DOI":"10.1007\/3-540-60218-6_31"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.: Module checking revisited. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_7"},{"key":"14_CR18","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Proc. of the Conf. on Logics of Programs (1985)","DOI":"10.1007\/3-540-15648-8_16"},{"key":"14_CR19","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254. Springer, Heidelberg (1997)","DOI":"10.1007\/3-540-63166-6_6"},{"key":"14_CR20","doi-asserted-by":"crossref","unstructured":"McMillan, K.L.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427. Springer, Heidelberg (1998)","DOI":"10.1007\/BFb0028738"},{"key":"14_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 342\u2013346. Springer, Heidelberg (1999)"},{"key":"14_CR22","doi-asserted-by":"crossref","unstructured":"Manna, Z., Pnueli, A.: Adequate proof principles for invariance and liveness properties of concurrent programs. Science of Computer Programming (1984)","DOI":"10.1016\/0167-6423(84)90003-0"},{"key":"14_CR23","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verfication of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verfication of Reactive Systems: Safety. Springer, Heidelberg (1995)"},{"key":"14_CR24","unstructured":"Pandya, P.: Compositional Verification of Distributed Programs. PhD thesis, University of Bombay (1988)"},{"key":"14_CR25","doi-asserted-by":"crossref","unstructured":"Pandya, P., Joseph, M.: P-A logic - a compositional proof system for distributed programs. Distributed Computing (1991)","DOI":"10.1007\/BF02311231"},{"key":"14_CR26","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: In transition from global to modular reasoning about programs. In: Logics and Models of Concurrent Systems. NATO ASI Series (1985)","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137. Springer, Heidelberg (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"14_CR29","doi-asserted-by":"crossref","unstructured":"Stark, E.: A proof technique for rely\/guarantee properties. In: Maheshwari, S.N. (ed.) FSTTCS 1985. LNCS, vol.\u00a0206. Springer, Heidelberg (1985)","DOI":"10.1007\/3-540-16042-6_21"},{"key":"14_CR30","doi-asserted-by":"crossref","unstructured":"Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol.\u00a0B. Elsevier and MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"14_CR31","unstructured":"Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification. In: IEEE Symposium on Logic in Computer Science (1986)"},{"key":"14_CR32","doi-asserted-by":"crossref","unstructured":"Zwiers, J., de Roever, W.P., van EmdeBoas, P.: Compositionality and concurrent networks: Soundness and completeness of a proof system. Technical Report, University of Nijmegen (1984)","DOI":"10.1007\/BFb0015776"},{"key":"14_CR33","series-title":"Lecture Notes in Computer Science","volume-title":"Compositionality, Concurrency, and Partial Correctness","year":"1989","unstructured":"Zwiers, J. (ed.): Compositionality, Concurrency, and Partial Correctness. LNCS, vol.\u00a0321. Springer, Heidelberg (1989)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/10722167_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,23]],"date-time":"2019-04-23T07:49:09Z","timestamp":1556005749000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/10722167_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540677703","9783540450474"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/10722167_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2000]]}}}