{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:56:54Z","timestamp":1762459014691,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642338250"},{"type":"electronic","value":"9783642338267"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33826-7_7","type":"book-chapter","created":{"date-parts":[[2012,9,25]],"date-time":"2012-09-25T22:46:25Z","timestamp":1348613185000},"page":"94-108","source":"Crossref","is-referenced-by-count":4,"title":["Compositional Reasoning about Shared Futures"],"prefix":"10.1007","author":[{"given":"Crystal Chang","family":"Din","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Johan","family":"Dovland","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olaf","family":"Owe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"7_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1109\/88.218170","volume":"1","author":"G. Agha","year":"1993","unstructured":"Agha, G., Fr\u00f8lund, S., Kim, W., Panwar, R., Patterson, A., Sturman, D.: Abstraction and modularity mechanisms for concurrent computing. IEEE Parallel Distributed Technology: Systems Applications\u00a01(2), 3\u201314 (1993)","journal-title":"IEEE Parallel Distributed Technology: Systems Applications"},{"issue":"3","key":"7_CR2","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/j.tcs.2007.09.002","volume":"389","author":"A. Ahern","year":"2007","unstructured":"Ahern, A., Yoshida, N.: Formalising Java RMI with explicit code mobility. Theoretical Computer Science\u00a0389(3), 341\u2013410 (2007)","journal-title":"Theoretical Computer Science"},{"key":"7_CR3","unstructured":"Falkner, K., Coddington, P.D., Oudshoorn, M.J.: Implementing asynchronous remote method invocation in Java. In: Proc. PART 1999 (November 1999)"},{"key":"7_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-13010-6_3","volume-title":"Advanced Lectures on Software Engineering","author":"B. Morandi","year":"2010","unstructured":"Morandi, B., Bauer, S.S., Meyer, B.: SCOOP \u2013 A Contract-Based Concurrent Object-Oriented Programming Model. In: M\u00fcller, P. (ed.) LASER Summer School 2007\/2008. LNCS, vol.\u00a06029, pp. 41\u201390. Springer, Heidelberg (2010)"},{"issue":"7","key":"7_CR5","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1016\/j.jlap.2009.01.001","volume":"78","author":"E. \u00c1brah\u00e1m","year":"2009","unstructured":"\u00c1brah\u00e1m, E., Grabe, I., Gr\u00fcner, A., Steffen, M.: Behavioral interface description of an object-oriented language with futures and promises. Journal of Logic and Algebraic Programming\u00a078(7), 491\u2013518 (2009)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"7_CR6","unstructured":"Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Science of Computer Programming (2010)"},{"issue":"4","key":"7_CR7","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B. Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. IPL\u00a021(4), 181\u2013185 (1985)","journal-title":"IPL"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Baker Jr., H.G., Hewitt, C.: The incremental garbage collection of processes. In: Proc. 1977 Symposium on Artificial Intelligence and Programming Languages, pp. 55\u201359. ACM (1977)","DOI":"10.1145\/872736.806932"},{"key":"7_CR9","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS (LNAI), vol.\u00a04334. Springer, Heidelberg (2007)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Broy, M., St\u00f8len, K.: Specification and Development of Interactive Systems. Monographs in Computer Science. Springer (2001)","DOI":"10.1007\/978-1-4613-0091-5"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"All About Maude - A High-Performance Logical Framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"key":"7_CR12","unstructured":"Dahl, O.-J.: Can program proving be made practical?. In: Les Fondements de la Programmation. Institut de Recherche d\u2019Informatique et d\u2019Automatique, Toulouse, France, pp. 57\u2013114 (1977)"},{"key":"7_CR13","first-page":"561","volume-title":"Research Directions in Object-Oriented Programming","author":"O.-J. Dahl","year":"1987","unstructured":"Dahl, O.-J.: Object-oriented specifications. In: Research Directions in Object-Oriented Programming, pp. 561\u2013576. MIT Press, Cambridge (1987)"},{"key":"7_CR14","unstructured":"Dahl, O.-J.: Verifiable Programming. International Series in Computer Science. Prentice Hall (1992)"},{"key":"7_CR15","unstructured":"Dahl, O.-J., Owe, O.: Formal methods and the RM-ODP. Research Report 261, Dept. of Informatics, University of Oslo, Norway (1998)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-540-71316-6_22","volume-title":"Programming Languages and Systems","author":"F.S. Boer de","year":"2007","unstructured":"de Boer, F.S., Clarke, D., Johnsen, E.B.: A Complete Guide to the Future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 316\u2013330. Springer, Heidelberg (2007)"},{"issue":"3","key":"7_CR17","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.jlap.2012.01.003","volume":"81","author":"C.C. Din","year":"2012","unstructured":"Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: Component reasoning for concurrent objects. Journal of Logic and Algebraic Programming\u00a081(3), 227\u2013256 (2012)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Din, C.C., Dovland, J., Owe, O.: An approach to compositional reasoning about concurrent objects and futures. Research Report 415, Dept. of Informatics, University of Oslo (2012), http:\/\/folk.uio.no\/crystald\/rr415.pdf","DOI":"10.1007\/978-3-642-33826-7_7"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Dovland, J., Johnsen, E.B., Owe, O.: Verification of concurrent objects with asynchronous method calls. In: Proc. SwSTE 2005, pp. 141\u2013150. IEEE Press (2005)","DOI":"10.1109\/SWSTE.2005.24"},{"issue":"4","key":"7_CR20","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/4472.4478","volume":"7","author":"R.H. Halstead Jr.","year":"1985","unstructured":"Halstead Jr., R.H.: Multilisp: a language for concurrent symbolic computation. ACM Trans. Program. Lang. Syst.\u00a07(4), 501\u2013538 (1985)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"7_CR21","unstructured":"Full ABS Modeling Framework, Deliverable 1.2 of project FP7-231620 (HATS) (March 2011), http:\/\/www.hats-project.eu"},{"key":"7_CR22","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice Hall (1985)"},{"key":"7_CR23","unstructured":"International Telecommunication Union. Open Distributed Processing - Reference Model parts 1\u20134. Technical report, ISO\/IEC, Geneva (1995)"},{"key":"7_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-540-31987-0_29","volume-title":"Programming Languages and Systems","author":"A. Jeffrey","year":"2005","unstructured":"Jeffrey, A., Rathke, J.: Java JR: Fully\u00a0Abstract\u00a0Trace\u00a0Semantics for\u00a0a\u00a0Core\u00a0Java\u00a0Language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 423\u2013438. Springer, Heidelberg (2005)"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-540-39993-3_9","volume-title":"From Object-Orientation to Formal Methods","author":"E.B. Johnsen","year":"2004","unstructured":"Johnsen, E.B., Owe, O.: Object-Oriented Specification and Open Distributed Systems. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From OO to FM (Dahl Festschrift). LNCS, vol.\u00a02635, pp. 137\u2013164. Springer, Heidelberg (2004)"},{"issue":"1","key":"7_CR26","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10270-006-0011-2","volume":"6","author":"E.B. Johnsen","year":"2007","unstructured":"Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling\u00a06(1), 35\u201358 (2007)","journal-title":"Software and Systems Modeling"},{"key":"7_CR27","doi-asserted-by":"crossref","unstructured":"Liskov, B.H., Shrira, L.: Promises: Linguistic support for efficient asynchronous procedure calls in distributed systems. In: Proc. PLDI 1988. ACM Press (1988)","DOI":"10.1145\/53990.54016"},{"key":"7_CR28","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science\u00a096, 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"7_CR29","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1145\/1780.1805","volume":"6","author":"N. Soundararajan","year":"1984","unstructured":"Soundararajan, N.: Axiomatic semantics of communicating sequential processes. ACM TOPLAS\u00a06(4), 647\u2013662 (1984)","journal-title":"ACM TOPLAS"},{"issue":"1-2","key":"7_CR30","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1016\/0304-3975(84)90122-1","volume":"31","author":"N. Soundararajan","year":"1984","unstructured":"Soundararajan, N.: A proof technique for parallel programs. Theoretical Computer Science\u00a031(1-2), 13\u201329 (1984)","journal-title":"Theoretical Computer Science"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Yonezawa, A., Briot, J.-P., Shibayama, E.: Object-oriented concurrent programming in ABCL\/1. In: Proc. OOPSLA 1986. Sigplan Notices, vol.\u00a021(11), pp. 258\u2013268 (1986)","DOI":"10.1145\/960112.28722"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33826-7_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T12:44:14Z","timestamp":1744202654000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33826-7_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642338250","9783642338267"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33826-7_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}