{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T16:09:28Z","timestamp":1742918968811,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642020520"},{"type":"electronic","value":"9783642020537"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-02053-7_15","type":"book-chapter","created":{"date-parts":[[2009,6,10]],"date-time":"2009-06-10T06:13:15Z","timestamp":1244614395000},"page":"288-305","source":"Crossref","is-referenced-by-count":4,"title":["Assume-Guarantee Verification of Concurrent Systems"],"prefix":"10.1007","author":[{"given":"Liliana","family":"D\u2019Errico","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michele","family":"Loreti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"15_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(93)90151-I","volume":"114","author":"M. Abadi","year":"1993","unstructured":"Abadi, M., Plotkin, G.D.: A logical view of composition. Theoretical Computer Science\u00a0114(1), 3\u201330 (1993)","journal-title":"Theoretical Computer Science"},{"key":"15_CR2","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1109\/LICS.1994.316076","volume-title":"Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science","author":"H.R. Andersen","year":"1994","unstructured":"Andersen, H.R., Stirling, C., Winskel, G.: A compositional proof system for the modal mu-calculus. In: Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France, July 4-7, pp. 144\u2013153. IEEE Computer Society, Los Alamitos (1994)"},{"key":"15_CR3","first-page":"94","volume":"95","author":"A. Antonik","year":"2008","unstructured":"Antonik, A., Huth, M., Larsen, K.G., Nyman, U., Wasowski, A.: 20 years of modal and mixed specifications. Bulletin of the EATCS\u00a095, 94\u2013129 (2008)","journal-title":"Bulletin of the EATCS"},{"issue":"1-3","key":"15_CR4","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0019-9958(84)80025-X","volume":"60","author":"J.A. Bergstra","year":"1984","unstructured":"Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Control\u00a060(1-3), 109\u2013137 (1984)","journal-title":"Information and Control"},{"issue":"3","key":"15_CR5","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1145\/828.833","volume":"31","author":"S.D. Brookes","year":"1984","unstructured":"Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM\u00a031(3), 560\u2013599 (1984)","journal-title":"J. ACM"},{"issue":"1-3","key":"15_CR6","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.tcs.2006.12.034","volume":"375","author":"S. Brookes","year":"2007","unstructured":"Brookes, S.: A semantics for concurrent separation logic. Theoretical Computer Science\u00a0375(1-3), 227\u2013270 (2007); Festschrift for John C. Reynolds\u2019s 70th birthday","journal-title":"Theoretical Computer Science"},{"issue":"2-3","key":"15_CR7","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/j.tcs.2006.01.020","volume":"358","author":"L. Caires","year":"2006","unstructured":"Caires, L., Lozes, \u00c9.: Elimination of quantifiers and undecidability in spatial logics for concurrency. Theor. Comput. Sci.\u00a0358(2-3), 293\u2013314 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR8","first-page":"1","volume-title":"Information and Computation","author":"L. Caires","year":"2001","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). In: Information and Computation, pp. 1\u201337. Springer, Heidelberg (2001)"},{"key":"15_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45694-5_15","volume-title":"CONCUR 2002 - Concurrency Theory","author":"L. Caires","year":"2002","unstructured":"Caires, L., Cardelli, L.: A spatial logic for concurrency (part II). In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol.\u00a02421, pp. 209\u2013225. Springer, Heidelberg (2002)"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","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, pp. 52\u201371. Springer, Heidelberg (1982)"},{"issue":"8","key":"15_CR11","first-page":"725","volume":"27","author":"R. Cleaveland","year":"1989","unstructured":"Cleaveland, R.: Tableau-based model checking in the propositional mu-calculus. Acta Inf.\u00a027(8), 725\u2013747 (1989)","journal-title":"Acta Inf."},{"key":"15_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/3-540-46562-6_22","volume-title":"Perspectives of System Informatics","author":"M. Dam","year":"2000","unstructured":"Dam, M., Gurov, D.: Compositional verification of CCS processes. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol.\u00a01755, pp. 247\u2013256. Springer, Heidelberg (2000)"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"D\u2019Errico, L., Loreti, M.: Assume-guarantee verification of concurrent systems. Technical report, Universit\u00e0 di Firenze (2009), http:\/\/www.dsi.unifi.it\/~loreti\/","DOI":"10.1007\/978-3-642-02053-7_15"},{"issue":"1","key":"15_CR14","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1145\/2455.2460","volume":"32","author":"M. Hennessy","year":"1985","unstructured":"Hennessy, M., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM\u00a032(1), 137\u2013161 (1985)","journal-title":"J. ACM"},{"key":"15_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2008.04.050","volume":"212","author":"T. Hoare","year":"2008","unstructured":"Hoare, T., O\u2019Hearn, P.: Separation logic semantics for communicating processes. Electronic Notes in Theoretical Computer Science\u00a0212, 3\u201325 (2008); Proceedings of the First International Conference on Foundations of Informatics, Computing and Software (FICS 2008)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"issue":"4","key":"15_CR16","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 Transactions on Programming Languages and Systems\u00a05(4), 596\u2013619 (1983)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"15_CR17","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theor. Comput. Sci.\u00a027, 333\u2013354 (1983)","journal-title":"Theor. Comput. Sci."},{"issue":"6","key":"15_CR18","doi-asserted-by":"publisher","first-page":"761","DOI":"10.1093\/logcom\/1.6.761","volume":"1","author":"K.G. Larsen","year":"1991","unstructured":"Larsen, K.G., Xinxin, L.: Compositionality through an operational semantics of contexts. J. Log. Comput.\u00a01(6), 761\u2013795 (1991)","journal-title":"J. Log. Comput."},{"key":"15_CR19","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":"15_CR20","volume-title":"Communication and concurrency","author":"R. Milner","year":"1989","unstructured":"Milner, R.: Communication and concurrency. Prentice-Hall, Inc., Upper Saddle River (1989)"},{"key":"15_CR21","doi-asserted-by":"publisher","first-page":"215","DOI":"10.2307\/421090","volume":"5","author":"P.W. O\u2019hearn","year":"1999","unstructured":"O\u2019hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic\u00a05, 215\u2013244 (1999)","journal-title":"Bulletin of Symbolic Logic"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Symposium on Logic in Computer Science, p. 55 (2002)","DOI":"10.1109\/LICS.2002.1029817"},{"key":"15_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-50939-9_144","volume-title":"TAPSOFT","author":"C. Stirling","year":"1989","unstructured":"Stirling, C., Walker, D.: Local model checking in the modal mu-calculus. In: D\u00edaz, J., Orejas, F. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol.\u00a0351, pp. 369\u2013383. Springer, Heidelberg (1989)"},{"key":"15_CR24","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The formal semantics of programming languages: an introduction","author":"G. Winskel","year":"1993","unstructured":"Winskel, G.: The formal semantics of programming languages: an introduction. MIT Press, Cambridge (1993)"}],"container-title":["Lecture Notes in Computer Science","Coordination Models and Languages"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-02053-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,10]],"date-time":"2025-02-10T02:09:17Z","timestamp":1739153357000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-02053-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642020520","9783642020537"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-02053-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}