{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T16:10:08Z","timestamp":1746375008839,"version":"3.40.4"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319108810"},{"type":"electronic","value":"9783319108827"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10882-7_17","type":"book-chapter","created":{"date-parts":[[2014,9,11]],"date-time":"2014-09-11T06:54:19Z","timestamp":1410418459000},"page":"277-294","source":"Crossref","is-referenced-by-count":2,"title":["Modular Reasoning for Message-Passing Programs"],"prefix":"10.1007","author":[{"given":"Jinjiang","family":"Lei","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zongyan","family":"Qiu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","unstructured":"Bickford, M., Constable, R.L.: A causal logic of events in formalized computational type theory (2005)"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-28644-8_2","volume-title":"CONCUR 2004 - Concurrency Theory","author":"S.D. Brookes","year":"2004","unstructured":"Brookes, S.D.: A semantics for concurrent separation logic. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol.\u00a03170, pp. 16\u201334. Springer, Heidelberg (2004)"},{"issue":"4","key":"17_CR3","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s004460050018","volume":"9","author":"B. Charron-Bost","year":"1996","unstructured":"Charron-Bost, B., Mattern, F., Tel, G.: Synchronous, asynchronous, and causally ordered communication. Distributed Computing\u00a09(4), 173\u2013191 (1996)","journal-title":"Distributed Computing"},{"key":"17_CR4","unstructured":"de Roever, W.-P., de Boer, F., Hanneman, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification: Introduction to Compositional and Noncompositional Proof Methods. Cambridge University Press (January 2012)"},{"issue":"8","key":"17_CR5","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"C.A.R. Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM\u00a021(8), 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"issue":"4","key":"17_CR6","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"C.B. Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst.\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR7","unstructured":"Kahn, G.: The semantics of simple language for parallel programming. In: IFIP Congress, pp. 471\u2013475 (1974)"},{"issue":"7","key":"17_CR8","doi-asserted-by":"publisher","first-page":"558","DOI":"10.1145\/359545.359563","volume":"21","author":"L. Lamport","year":"1978","unstructured":"Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM\u00a021(7), 558\u2013565 (1978)","journal-title":"Commun. ACM"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Lei, J., Qiu, Z.: Modular reasoning for message-passing programs. Technical report, School of Mathematical Sciences, Peking University (June 2014), https:\/\/sites.google.com\/site\/jinjianglei\/publications\/rgdsep.","DOI":"10.1007\/978-3-319-10882-7_17"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3","volume-title":"A Calculus of Communication Systems","author":"R. Milner","year":"1980","unstructured":"Milner, R.: A Calculus of Communication Systems. LNCS, vol.\u00a092. Springer, Heidelberg (1980)"},{"key":"17_CR11","unstructured":"Milner, R.: Communication and concurrency. PHI Series in computer science. Prentice Hall (1989)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Milner, R.: The polyadic pi-calculus (abstract). In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, p. 1. Springer, Heidelberg (1992)","DOI":"10.1007\/BFb0084778"},{"key":"17_CR13","unstructured":"Milner, R.: Communicating and mobile systems - the Pi-calculus. Cambridge University Press (1999)"},{"key":"17_CR14","doi-asserted-by":"crossref","unstructured":"Parkinson, M.J., Bornat, R., Calcagno, C.: Variables as resource in hoare logics. In: LICS, pp. 137\u2013146 (2006)","DOI":"10.1109\/LICS.2006.52"},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Reddy, U.S., Reynolds, J.C.: Syntactic control of interference for separation logic. In: POPL, pp. 323\u2013336 (2012)","DOI":"10.1145\/2103656.2103695"},{"key":"17_CR16","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS, pp. 55\u201374 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"17_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.J.: A marriage of rely\/guarantee and separation logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/978-3-642-10672-9_15","volume-title":"Programming Languages and Systems","author":"J. Villard","year":"2009","unstructured":"Villard, J., Lozes, \u00c9., Calcagno, C.: Proving copyless message passing. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 194\u2013209. Springer, Heidelberg (2009)"},{"issue":"17","key":"17_CR19","doi-asserted-by":"publisher","first-page":"1001","DOI":"10.1016\/j.ipl.2009.06.003","volume":"109","author":"I. Wehrman","year":"2009","unstructured":"Wehrman, I., Hoare, C.A.R., O\u2019Hearn, P.W.: Graphical models of separation logic. Inf. Process. Lett.\u00a0109(17), 1001\u20131004 (2009)","journal-title":"Inf. Process. Lett."}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2014"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10882-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T15:44:34Z","timestamp":1746373474000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10882-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319108810","9783319108827"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10882-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}