{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T07:20:11Z","timestamp":1771485611967,"version":"3.50.1"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2015,5,1]],"date-time":"2015-05-01T00:00:00Z","timestamp":1430438400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2015,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. The\n            <jats:italic>future mechanism<\/jats:italic>\n            extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed environment. However, futures add a level of complexity to program analysis, as the program semantics becomes more involved. This paper presents a model for asynchronously communicating objects, where return values from method calls are handled by futures. The model facilitates invariant specifications over the locally visible communication history of each object. Compositional reasoning is supported and proved sound, as each object may be specified and verified independently of its environment. A kernel object-oriented language with futures inspired by the ABS modeling language is considered. A compositional proof system for this language is presented, formulated within dynamic logic.\n          <\/jats:p>","DOI":"10.1007\/s00165-014-0322-y","type":"journal-article","created":{"date-parts":[[2014,11,21]],"date-time":"2014-11-21T16:07:13Z","timestamp":1416586033000},"page":"551-572","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":31,"title":["Compositional reasoning about active objects with shared futures"],"prefix":"10.1145","volume":"27","author":[{"given":"Crystal Chang","family":"Din","sequence":"first","affiliation":[{"name":"Department of Computer Science, Technische Universit\u00e4t Darmstadt, Darmstadt, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olaf","family":"Owe","sequence":"additional","affiliation":[{"name":"Department of Informatics, University of Oslo, Oslo, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Ahrendt W Dylla M (2012) A system for compositional verification of asynchronous objects. Sci Comput Program. 77(12):1289-1309. doi:10.1016\/j.scico.2010.08.003","DOI":"10.1016\/j.scico.2010.08.003"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/88.218170"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2009.01.001"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Ahern A Yoshida N (2007) Formalising java rmi with explicit code mobility. Theor Comput Sci 389(3):341\u2013410. Semantic and Logical Foundations of Global Computing","DOI":"10.1016\/j.tcs.2007.09.002"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Beckert B H\u00e4hnle R Schmitt PH (eds) (2007) Verification of object-oriented software: the KeY approach. LNCS vol 4334. Springer Berlin","DOI":"10.1007\/978-3-540-69061-0"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Baker Jr HG Hewitt C (1977) The incremental garbage collection of processes. In: Proceedings of the 1977 symposium on artificial intelligence and programming languages New York NY USA. ACM pp 55\u201359","DOI":"10.1145\/872736.806932"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-008-0096-1"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.5555\/374869"},{"key":"e_1_2_1_2_10_2","unstructured":"Clavel M Dur\u00e1n F Eker S Lincoln P Mart\u00ed-Oliet N Meseguer J Talcott CL (2007) All about Maude\u2014a high-performance logical framework how to specify program and verify systems in rewriting logic. LNCS vol 4350. Springer Berlin"},{"key":"e_1_2_1_2_11_2","unstructured":"Dahl O-J (1977) Can program proving be made practical? In: Amirchahy M N\u00e9el D (eds) Les Fondements de la Programmation. Institut de Recherche d\u2019Informatique et d\u2019Automatique Toulouse France December 1977 pp 57\u2013114"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Dahl O-J (1987) Object-oriented specifications. In: Research directions in object-oriented programming. MIT Press Cambridge pp 561\u2013576","DOI":"10.1145\/323779.323761"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/530986"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00304-2"},{"key":"#cr-split#-e_1_2_1_2_15_2.1","doi-asserted-by":"crossref","unstructured":"de Boer FS Clarke D Johnsen EB (2007) A complete guide to the future. In: de Nicola R","DOI":"10.1007\/978-3-540-71316-6_22"},{"key":"#cr-split#-e_1_2_1_2_15_2.2","unstructured":"(ed) Proceedings of the 16th European symposium on programming (ESOP'07) March 2007. LNCS vol 4421. Springer Berlin pp 316-330"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2012.01.003"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Din CC Dovland J Owe O (2012) An approach to compositional reasoning about concurrent objects and futures. Research Report 415 Department of Informatics University of Oslo February 2012. http:\/\/urn.nb.no\/URN:NBN:no-30589","DOI":"10.1007\/978-3-642-33826-7_7"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Din CC Dovland J Owe O (2012) Compositional reasoning about shared futures. In: Eleftherakis G Hinchey M Holcombe M (eds) Proceedings of the international conference on software engineering and formal methods (SEFM\u201912). LNCS vol 7504. Springer Berlin pp 94\u2013108","DOI":"10.1007\/978-3-642-33826-7_7"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1327452.1327492"},{"key":"e_1_2_1_2_20_2","unstructured":"Dovland J Johnsen EB Owe O (2005) Verification of concurrent objects with asynchronous method calls. In: Proceedings of the IEEE international conference on software science technology and engineering (SwSTE\u201905) February 2005. IEEE Computer Society Press pp 141\u2013150"},{"key":"e_1_2_1_2_21_2","unstructured":"Dahl O-J Owe O (1998) Formal methods and the RM-ODP. Research Report 261 Department of Informatics University of Oslo Norway May 1998"},{"key":"e_1_2_1_2_22_2","unstructured":"de Roever W-P de Boer F Hannemann U Hooman J Lakhnech Y Poel M Zwiers J (2001) Concurrency verification: introduction to compositional and noncompositional methods. Cambridge University Press New York"},{"key":"e_1_2_1_2_23_2","unstructured":"Falkner KEK Coddington PD Oudshoorn MJ (1999) Implementing asynchronous remote method invocation in java"},{"key":"e_1_2_1_2_24_2","unstructured":"Full ABS Modeling Framework (2011). Deliverable 1.2 of project FP7-231620 (HATS). http:\/\/www.hats-project.eu"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"publisher","DOI":"10.1145\/4472.4478"},{"key":"e_1_2_1_2_26_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_27_2","unstructured":"International Telecommunication Union (1995) Open distributed processing-reference model parts 1\u20134. Technical report ISO\/IEC Geneva July 1995"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Johnsen EB Owe O (2004) Object-oriented specification and open distributed systems. In: Owe O Krogdahl S Lyche T (eds) From object-orientation to formal methods: essays in memory of Ole-Johan Dahl. LNCS vol 2635. Springer Berlin pp 137\u2013164","DOI":"10.1007\/978-3-540-39993-3_9"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-006-0011-2"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Jeffrey ASA Rathke J (2005) Java Jr.: fully abstract trace semantics for a core Java language. In: Proceedings of the European symposium on programming. LNCS vol 3444. Springer Berlin pp 423\u2013438","DOI":"10.1007\/978-3-540-31987-0_29"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Liskov BH Shrira L (1988) Promises: linguistic support for efficient asynchronous procedure calls in distributed systems. In: Wise DS (ed) Proceedings of the SIGPLAN conference on programming language design and implementation (PLDI\u201988). ACM Press pp 260\u2013267","DOI":"10.1145\/960116.54016"},{"key":"#cr-split#-e_1_2_1_2_32_2.1","unstructured":"Morandi B Bauer SS Meyer B (2008) SCOOP-a contract-based concurrent object-oriented programming model. In: M\u00fcller P"},{"key":"#cr-split#-e_1_2_1_2_32_2.2","unstructured":"(ed) Advanced lectures on software engineering LASER Summer School 2007\/2008. Lecture notes in computer science vol 6029. Springer Berlin pp 41-90"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/162685.162705"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/261119"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/1780.1805"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90122-1"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Yonezawa A Briot J-P Shibayama E (1986) Object-oriented concurrent programming in ABCL\/1. In: Conference on object-oriented programming systems languages and applications (OOPSLA\u201986). Sigplan Notices vol 21 no 11 pp 258\u2013268 November 1986","DOI":"10.1145\/960112.28722"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-014-0322-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-014-0322-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-014-0322-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:05:18Z","timestamp":1641485118000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-014-0322-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2015,5]]}},"alternative-id":["10.1007\/s00165-014-0322-y"],"URL":"https:\/\/doi.org\/10.1007\/s00165-014-0322-y","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5]]}}}