{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:56:55Z","timestamp":1725663415488},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540542339"},{"type":"electronic","value":"9783540475163"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54233-7_127","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:39:19Z","timestamp":1330209559000},"page":"93-114","source":"Crossref","is-referenced-by-count":3,"title":["Program composition and modular verification"],"prefix":"10.1007","author":[{"given":"Limor","family":"Fix","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nissim","family":"Francez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,8]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"K.R. Apt, F.S. de Boer, E.-R. Olderog: \u201cProving termination of parallel programs,\u201d in W. Feijen, N. van Gasteren, D. Gries, J. Misra (eds.): \u201cBeauty is our business, a birth-day salute to Edsger W. Dijkstra,\u201d Springer-Verlag, 1990. Also: TR CS-R9016, CWI Amsterdam May 1990.","DOI":"10.1007\/978-1-4612-4476-9_1"},{"key":"7_CR2","unstructured":"A.V. Aho, J.E. Hopcropf, J.D. Ullman: \u201cThe design and analysis of computer algorithms,\u201d Addison-Wesley, 1974."},{"issue":"1","key":"7_CR3","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1145\/322358.322372","volume":"30","author":"K.R. Apt","year":"1983","unstructured":"K.R. Apt: \u201cFormal justification of a proof system for communication sequential processes,\u201d Journal of the ACM, vol. 30, No. 1, January 1983, pp. 197\u2013216.","journal-title":"Journal of the ACM"},{"key":"7_CR4","doi-asserted-by":"crossref","unstructured":"L. Bouge, N. Francez: \u201cA Compositional Approach to Superimposition,\u201d 15th ACM Symp. on Principles of Programming Languages, San Diego, CA, January 1988.","DOI":"10.1145\/73560.73581"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"M. Chandy, J. Misra: \u201cParallel programs design,\u201d Addison-Wesly, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"7_CR6","doi-asserted-by":"crossref","first-page":"217","DOI":"10.1016\/0020-0190(83)90092-3","volume":"16","author":"E.W. Dijkstra","year":"1983","unstructured":"E.W. Dijkstra, W.H.J. Feijen, A.J.M. van Gasteren: \u201cDerivation of a termination detection algorithm for distributed computations,\u201d IPL 16, pp. 217\u2013219, 1983.","journal-title":"IPL"},{"key":"7_CR7","unstructured":"N. Francez, I.R. Forman: \u201cSuperimposition for interacting processes,\u201d CONCUR'90, Amsterdam, August 1990. LNCS 458 J.C.M. Baeten, J.W. Klop (Eds.), Springer-Verlag, 1990."},{"key":"7_CR8","unstructured":"L. Fix, N. Francez, O. Grumberg: \u201cSemantics-driven decompositions for the verification of distributed programs,\u201d Proc. of the IFIP working group 2.2\/2.3 working conference on Programming concepts and Methods, Sea of Galilee, Israel, April 1990, North-Holland, pp. 101\u2013123."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"N. Francez: \u201cFairness,\u201d Springer-Verlag, 1986.","DOI":"10.1007\/978-1-4612-4886-6"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"E. Gafni: \u201cPerspectives on Distributed Network Protocols: A Case for Building Blocks,\u201d MILCON 86, Monterey, Ca., October 1986.","DOI":"10.1109\/MILCOM.1986.4805648"},{"issue":"8","key":"7_CR11","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"C.A.R. Hoare: \u201cCommunicating sequential processes,\u201d CACM 21, 8, August 1978, pp. 666\u2013677.","journal-title":"CACM"},{"key":"7_CR12","unstructured":"S. Katz: \u201cA Superimposition Control Construct for Distributed Systems\u201d, submitted to Transaction on Programming Languages and Systems. Preliminary version MCC technical Report STP-268-87."},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"J. Misra, M. Chandy: \u201cProofs of networks of processes,\u201d IEEE SE 7(4), 1981.","DOI":"10.1109\/TSE.1981.230844"},{"key":"7_CR14","unstructured":"J. Misra: \u201cPreserving progress under program composition,\u201d Notes on UNITY: 17\u201320."},{"key":"7_CR15","doi-asserted-by":"crossref","unstructured":"S. Owicki, D. Gries: \u201cAn axiomatic proof technique for parallel programs,\u201d Acta Informatica 6, 1976.","DOI":"10.1007\/BF00268134"},{"key":"7_CR16","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1016\/0020-0190(90)90073-7","volume":"36","author":"S. Ramesh","year":"1990","unstructured":"S. Ramesh: \u201cOn the completeness of modular proof systems,\u201d IPL 36, pp. 195\u2013201, 1990.","journal-title":"IPL"},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"C. Stirling: \u201cA generalization of Owicki-Gries's Hoare logic for a concurrent while language,\u201d Theoretical computer science no. 58 pp. 347\u2013359, 1988.","DOI":"10.1016\/0304-3975(88)90033-3"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"J. Zwiers, W.P. de Roever, P. van Emde Boas: \u201cCompositionality and concurrent networks: soundness and completeness of a proof system,\u201d Proc. 12th ICALP, Nafplion, Greece, July 1985, Springer LNCS 194, pp. 509\u2013519.","DOI":"10.1007\/BFb0015776"},{"key":"7_CR19","unstructured":"J. Zwiers: \u201cCompositionality, concurrency and partial correctness,\u201d Springer LNCS 321, 1989."}],"container-title":["Lecture Notes in Computer Science","Automata, Languages and Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54233-7_127.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T03:42:58Z","timestamp":1640922178000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54233-7_127"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540542339","9783540475163"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-54233-7_127","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}