{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T07:16:12Z","timestamp":1771485372317,"version":"3.50.1"},"publisher-location":"Cham","reference-count":61,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030643539","type":"print"},{"value":"9783030643546","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-64354-6_4","type":"book-chapter","created":{"date-parts":[[2020,12,8]],"date-time":"2020-12-08T09:12:03Z","timestamp":1607418723000},"page":"85-121","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Behavioral Contracts for Cooperative Scheduling"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0996-2543","authenticated-orcid":false,"given":"Eduard","family":"Kamburjan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3588-5609","authenticated-orcid":false,"given":"Crystal Chang","family":"Din","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8000-7613","authenticated-orcid":false,"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5382-3949","authenticated-orcid":false,"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,12,4]]},"reference":[{"issue":"3","key":"4_CR1","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1145\/203095.201069","volume":"17","author":"M Abadi","year":"1995","unstructured":"Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3), 507\u2013534 (1995)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR2","unstructured":"ABS development team: The ABS language specification, January 2018. http:\/\/docs.abs-models.org\/"},{"key":"4_CR3","first-page":"49","volume-title":"Research Directions in Object-Oriented Programming","author":"G Agha","year":"1987","unstructured":"Agha, G., Hewitt, C.: Actors: a conceptual foundation for concurrent object-oriented programming. In: Shriver, B. (ed.) Research Directions in Object-Oriented Programming, pp. 49\u201374. MIT Press, Cambridge (1987)"},{"key":"4_CR4","series-title":"From Theory to Practice","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): LNCS. From Theory to Practice, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"issue":"12","key":"4_CR5","doi-asserted-by":"publisher","first-page":"1289","DOI":"10.1016\/j.scico.2010.08.003","volume":"77","author":"W Ahrendt","year":"2012","unstructured":"Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289\u20131309 (2012)","journal-title":"Sci. Comput. Program."},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-33427-6_7","volume-title":"Service-Oriented and Cloud Computing","author":"FS de Boer","year":"2012","unstructured":"de Boer, F.S., H\u00e4hnle, R., Johnsen, E.B., Schlatte, R., Wong, P.Y.H.: Formal modeling of resource management for cloud architectures: an industrial case study. In: De Paoli, F., Pimentel, E., Zavattaro, G. (eds.) ESOCC 2012. LNCS, vol. 7592, pp. 91\u2013106. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-33427-6_7"},{"issue":"2","key":"4_CR7","doi-asserted-by":"publisher","first-page":"11:1","DOI":"10.1145\/2824255","volume":"17","author":"E Albert","year":"2016","unstructured":"Albert, E., Flores-Montoya, A., Genaim, S., Martin-Martin, E.: May-happen-in-parallel analysis for actor-based concurrency. ACM Trans. Comput. Log. 17(2), 11:1\u201311:39 (2016)","journal-title":"ACM Trans. Comput. Log."},{"key":"4_CR8","unstructured":"Armstrong, J.: Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf Series, Pragmatic Bookshelf (2007)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/11808107_4","volume-title":"Dependable Systems: Software, Computing, Networks","author":"V Arslan","year":"2006","unstructured":"Arslan, V., Eugster, P., Nienaltowski, P., Vaucouleur, S.: SCOOP \u2013 concurrency made easy. In: Kohlas, J., Meyer, B., Schiper, A. (eds.) Dependable Systems: Software, Computing, Networks. LNCS, vol. 4028, pp. 82\u2013102. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11808107_4"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Baker, H.G., Hewitt, C.E.: The incremental garbage collection of processes. In: Proceeding of the Symposium on Artificial Intelligence Programming Languages, number 12 in SIGPLAN Notices, p. 11, August 1977","DOI":"10.1145\/800228.806932"},{"key":"4_CR11","unstructured":"Baudin, P., et al.: ACSL: ANSI\/ISO C Specification Language. CEA LIST and INRIA, 1.4 edition (2010)"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification - specification is the new bottleneck. In: Cassez, F., Huuck, R., Klein, G., Schlich, B., (eds.) Proceedings 7th Conference on Systems Software Verification, EPTCS, vol. 102, pp. 18\u201332 (2012)","DOI":"10.4204\/EPTCS.102.4"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1007\/3-540-45165-X_2","volume-title":"Java on Smart Cards: Programming and Security","author":"B Beckert","year":"2001","unstructured":"Beckert, B.: A dynamic logic for the formal verification of java card programs. In: Attali, I., Jensen, T. (eds.) JavaCard 2000. LNCS, vol. 2041, pp. 6\u201324. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45165-X_2"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-49812-6_3","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"B Beckert","year":"2016","unstructured":"Beckert, B., Klebanov, V., Wei\u00df, B.: Dynamic logic for java. Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 49\u2013106. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_3"},{"key":"4_CR15","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1016\/j.scico.2014.03.013","volume":"95","author":"S Blom","year":"2014","unstructured":"Blom, S., Huisman, M., Mihelcic, M.: Specification and verification of GPGPU programs. Sci. Comput. Program. 95, 376\u2013388 (2014)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"4_CR16","first-page":"61","volume":"22","author":"L Bocchi","year":"2012","unstructured":"Bocchi, L., Lange, J., Tuosto, E.: Three algorithms and a methodology for amending contracts for choreographies. Sci. Ann. Comp. Sci. 22(1), 61\u2013104 (2012)","journal-title":"Sci. Ann. Comp. Sci."},{"issue":"3","key":"4_CR17","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/2984450.2984457","volume":"3","author":"S Brookes","year":"2016","unstructured":"Brookes, S., O\u2019Hearn, P.W.: Concurrent separation logic. ACM SIGLOG News 3(3), 47\u201365 (2016)","journal-title":"ACM SIGLOG News"},{"key":"4_CR18","doi-asserted-by":"crossref","unstructured":"Caromel, D., Henrio, L., Serpette, B.P.: Asynchronous and deterministic objects. In: Proceedings of the 31st ACM Symposium on Principles of Programming Languages (POPL 2004), pp. 123\u2013134. ACM Press (2004)","DOI":"10.1145\/982962.964012"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-662-44202-9_9","volume-title":"ECOOP 2014 \u2013 Object-Oriented Programming","author":"P da Rocha Pinto","year":"2014","unstructured":"da Rocha Pinto, P., Dinsdale-Young, T., Gardner, P.: TaDA: a logic for time and data abstraction. In: Jones, R. (ed.) ECOOP 2014. LNCS, vol. 8586, pp. 207\u2013231. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44202-9_9"},{"key":"4_CR20","unstructured":"Dahl, O.-J.: Monitors revisited. In: Roscoe, A.W., (ed.) A classical Mind: Essays in Honour of C.A.R. Hoare, pp. 93\u2013103. Prentice Hall, Upper Saddle River (1994)"},{"issue":"5","key":"4_CR21","doi-asserted-by":"publisher","first-page":"76:1","DOI":"10.1145\/3122848","volume":"50","author":"F de Boer","year":"2017","unstructured":"de Boer, F., et al.: A survey of active object languages. ACM Comput. Surv. 50(5), 76:1\u201376:39 (2017)","journal-title":"ACM Comput. Surv."},{"key":"4_CR22","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":"FS de Boer","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. 4421, pp. 316\u2013330. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_22"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"517","DOI":"10.1007\/978-3-319-21401-6_35","volume-title":"Automated Deduction - CADE-25","author":"CC Din","year":"2015","unstructured":"Din, C.C., Bubel, R., H\u00e4hnle, R.: KeY-ABS: a deductive verification tool for the concurrent modelling language ABS. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 517\u2013526. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_35"},{"issue":"3","key":"4_CR24","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1016\/j.jlap.2012.01.003","volume":"81","author":"CC Din","year":"2012","unstructured":"Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: component reasoning for concurrent objects. J. Logic Algebraic Program. 81(3), 227\u2013256 (2012)","journal-title":"J. Logic Algebraic Program."},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-319-66902-1_2","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"CC Din","year":"2017","unstructured":"Din, C.C., H\u00e4hnle, R., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: Locally abstract, globally concrete semantics of concurrent programming languages. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS (LNAI), vol. 10501, pp. 22\u201343. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66902-1_2"},{"issue":"3","key":"4_CR26","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00165-014-0322-y","volume":"27","author":"CC Din","year":"2015","unstructured":"Din, C.C., Owe, O.: Compositional reasoning about active objects with shared futures. Formal Aspects Comput. 27(3), 551\u2013572 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0322-y","journal-title":"Formal Aspects Comput."},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-319-25423-4_14","volume-title":"Formal Methods and Software Engineering","author":"CC Din","year":"2015","unstructured":"Din, C.C., Tapia Tarifa, S.L., H\u00e4hnle, R., Johnsen, E.B.: History-based specification and verification of scalable concurrent and distributed systems. In: Butler, M., Conchon, S., Za\u00efdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 217\u2013233. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25423-4_14"},{"key":"4_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jlamp.2018.03.003","volume":"98","author":"T Dinsdale-Young","year":"2018","unstructured":"Dinsdale-Young, T., da Rocha Pinto, P., Gardner, P.: A perspective on specifying and verifying concurrent modules. J. Logic. Algebraic Methods Program. 98, 1\u201325 (2018)","journal-title":"J. Logic. Algebraic Methods Program."},{"issue":"1","key":"4_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0956796899003329","volume":"9","author":"C Flanagan","year":"1999","unstructured":"Flanagan, C., Felleisen, M.: The semantics of future and an application. J. Funct. Program. 9(1), 1\u201331 (1999)","journal-title":"J. Funct. Program."},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-642-38592-6_19","volume-title":"Formal Techniques for Distributed Systems","author":"AE Flores-Montoya","year":"2013","unstructured":"Flores-Montoya, A.E., Albert, E., Genaim, S.: May-happen-in-parallel based deadlock analysis for concurrent objects. In: Beyer, D., Boreale, M. (eds.) FMOODS\/FORTE -2013. LNCS, vol. 7892, pp. 273\u2013288. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-38592-6_19"},{"key":"4_CR31","unstructured":"Gavran, I., Niksic, F., Kanade, A., Majumdar, R., Vafeiadis, V.: Rely\/guarantee reasoning for asynchronous programs. In: Aceto, L., de Frutos Escrig, D., (eds.) 26th International Conference on Concurrency Theory (CONCUR 2015), volume 42 of Leibniz International Proceedings in Informatics (LIPIcs), pp. 483\u2013496. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015)"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science","author":"R H\u00e4hnle","year":"2019","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18"},{"issue":"4","key":"4_CR33","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1145\/4472.4478","volume":"7","author":"RH Halstead Jr","year":"1985","unstructured":"Halstead Jr., R.H.: Multilisp: a language for concurrent symbolic computation. ACM Trans. Program. Lang. Syst. 7(4), 501\u2013538 (1985)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"7","key":"4_CR34","doi-asserted-by":"publisher","first-page":"574","DOI":"10.1145\/361454.361473","volume":"15","author":"PB Hansen","year":"1972","unstructured":"Hansen, P.B.: Structured multiprogramming. Commun. ACM 15(7), 574\u2013578 (1972)","journal-title":"Commun. ACM"},{"key":"4_CR35","volume-title":"Operating System Principles","author":"PB Hansen","year":"1973","unstructured":"Hansen, P.B.: Operating System Principles. Prentice-Hall Inc, Upper Saddle River (1973)"},{"key":"4_CR36","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-1-4757-3472-0_6","volume-title":"Operating System Techniques","author":"CAR Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Towards a theory of parallel programming. In: Hansen, P.B. (ed.) Operating System Techniques, pp. 61\u201371. Springer, New York (1972). https:\/\/doi.org\/10.1007\/978-1-4757-3472-0_6"},{"key":"4_CR37","doi-asserted-by":"crossref","unstructured":"Honda, K., Yoshida, N., Carbone, M.: Multiparty asynchronous session types. In: Proceedings of the 35th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2008, pp. 273\u2013284 (2008)","DOI":"10.1145\/1328897.1328472"},{"issue":"1","key":"4_CR38","doi-asserted-by":"publisher","first-page":"3:1","DOI":"10.1145\/2873052","volume":"49","author":"H H\u00fcttel","year":"2016","unstructured":"H\u00fcttel, H., et al.: Foundations of session types and behavioural contracts. ACM Comput. Surv. 49(1), 3:1\u20133:36 (2016)","journal-title":"ACM Comput. Surv."},{"key":"4_CR39","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven, August 2008"},{"key":"4_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"EB Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142\u2013164. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25271-6_8"},{"issue":"4","key":"4_CR41","doi-asserted-by":"publisher","first-page":"596","DOI":"10.1145\/69575.69577","volume":"5","author":"CB Jones","year":"1983","unstructured":"Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596\u2013619 (1983)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"4_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-030-29026-9_22","volume-title":"Automated Reasoning with Analytic Tableaux and Related Methods","author":"E Kamburjan","year":"2019","unstructured":"Kamburjan, E.: Behavioral program logic. In: Cerrito, S., Popescu, A. (eds.) TABLEAUX 2019. LNCS (LNAI), vol. 11714, pp. 391\u2013408. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29026-9_22"},{"key":"4_CR43","unstructured":"Kamburjan, E.: Behavioral program logic and LAGC semantics without continuations (technical report). CoRR, abs\/1904.13338 (2019)"},{"key":"4_CR44","unstructured":"Kamburjan, E.: Modular verification of a modular specification: behavioral types as program logics. Ph.D. thesis, Technische Universit\u00e4t Darmstadt (2020)"},{"key":"4_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-98938-9_13","volume-title":"Integrated Formal Methods","author":"E Kamburjan","year":"2018","unstructured":"Kamburjan, E., Chen, T.-C.: Stateful behavioral types for active objects. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 214\u2013235. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_13"},{"key":"4_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"296","DOI":"10.1007\/978-3-319-47846-3_19","volume-title":"Formal Methods and Software Engineering","author":"E Kamburjan","year":"2016","unstructured":"Kamburjan, E., Din, C.C., Chen, T.-C.: Session-based compositional analysis for actor-based languages using futures. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 296\u2013312. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47846-3_19"},{"key":"4_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-030-30446-1_3","volume-title":"Software Engineering and Formal Methods","author":"E Kamburjan","year":"2019","unstructured":"Kamburjan, E., Din, C.C., H\u00e4hnle, R., Johnsen, E.B.: Asynchronous cooperative contracts for cooperative scheduling. In: \u00d6lveczky, P.C., Sala\u00fcn, G. (eds.) SEFM 2019. LNCS, vol. 11724, pp. 48\u201366. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_3"},{"key":"4_CR48","unstructured":"Kamburjan, E., Din, C.C., H\u00e4hnle, R., Johnsen, E.B.: Asynchronous cooperative contracts for cooperative scheduling. Technical report, TU Darmstadt (2019). http:\/\/formbar.raillab.de\/en\/techreportcontract\/"},{"issue":"3","key":"4_CR49","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015). https:\/\/doi.org\/10.1007\/s00165-014-0326-7","journal-title":"Formal Aspects Comput."},{"key":"4_CR50","unstructured":"Leavens, G.T., et al.: JML reference manual. Draft revision 2344, May 2013"},{"key":"4_CR51","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: The Dafny integrated development environment. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) Proceedings 1st Workshop on Formal Integrated Development Environment, F-IDE, EPTCS, Grenoble, France, vol. 149, pp. 3\u201315 (2014)","DOI":"10.4204\/EPTCS.149.0"},{"key":"4_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-662-49665-7_4","volume-title":"Fundamental Approaches to Software Engineering","author":"J-C Lin","year":"2016","unstructured":"Lin, J.-C., Yu, I.C., Johnsen, E.B., Lee, M.-C.: ABS-YARN: a formal framework for modeling Hadoop YARN clusters. In: Stevens, P., W\u0105sowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 49\u201365. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49665-7_4"},{"key":"4_CR53","doi-asserted-by":"crossref","unstructured":"Liskov, B.H., Shrira, L.: Promises: linguistic support for efficient asynchronous procedure calls in distributed systems. In: Wise, D.S. (ed.) Proceedings of the SIGPLAN Conference on Programming Language Design and Implementation (PLDI 1988), pp. 260\u2013267. ACM Press, June 1988","DOI":"10.1145\/960116.54016"},{"issue":"1","key":"4_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-11(1:1)2015","volume":"11","author":"K Nakata","year":"2015","unstructured":"Nakata, K., Uustalu, T.: A Hoare logic for the coinductive trace-based big-step semantics of while. Logical Methods Comput. Sci. 11(1), 1\u201332 (2015)","journal-title":"Logical Methods Comput. Sci."},{"key":"4_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44802-0_1","volume-title":"Computer Science Logic","author":"P O\u2019Hearn","year":"2001","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1"},{"key":"4_CR56","doi-asserted-by":"crossref","unstructured":"Oortwijn, W., Blom, S., Huisman, M.: Future-based static analysis of message passing programs. In: Orchard, D.A., Yoshida, N., (eds.) Proceedings of the Ninth workshop on Programming Language Approaches to Concurrency- and Communication-cEntric Software, PLACES 2016, EPTCS, Eindhoven, The Netherlands, 8th April 2016, vol. 211, pp. 65\u201372 (2016)","DOI":"10.4204\/EPTCS.211.7"},{"key":"4_CR57","doi-asserted-by":"publisher","first-page":"699","DOI":"10.1007\/978-3-662-49498-1_27","volume-title":"Programming Languages and Systems","author":"AJ Summers","year":"2016","unstructured":"Summers, A.J., M\u00fcller, P.: Actor services - modular verification of message passing programs. In: Thiemann, P. (ed.) ESOP 2016), vol. 9632, pp. 699\u2013726. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_27"},{"key":"4_CR58","unstructured":"Wei\u00df, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (2011)"},{"key":"4_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-31762-0_5","volume-title":"Formal Verification of Object-Oriented Software","author":"PYH Wong","year":"2012","unstructured":"Wong, P.Y.H., Diakov, N., Schaefer, I.: Modelling adaptable distributed object oriented systems using the HATS approach: a fredhopper case study. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol. 7421, pp. 49\u201366. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31762-0_5"},{"key":"4_CR60","doi-asserted-by":"crossref","unstructured":"Yonezawa, A., Briot, J.P., Shibayama, E.: Object-oriented concurrent programming in ABCL\/1. In: Conference on Object-Oriented Programming Systems, Languages and Applications (OOPSLA 1986), vol. 21, no. 11, pp. 258\u2013268, November 1986. SIGPLAN Notices","DOI":"10.1145\/960112.28722"},{"key":"4_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-54804-8_16","volume-title":"Fundamental Approaches to Software Engineering","author":"M Zaharieva-Stojanovski","year":"2014","unstructured":"Zaharieva-Stojanovski, M., Huisman, M.: Verifying class invariants in concurrent programs. In: Gnesi, S., Rensink, A. (eds.) FASE 2014. LNCS, vol. 8411, pp. 230\u2013245. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54804-8_16"}],"container-title":["Lecture Notes in Computer Science","Deductive Software Verification: Future Perspectives"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-64354-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,8]],"date-time":"2020-12-08T09:22:35Z","timestamp":1607419355000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-64354-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030643539","9783030643546"],"references-count":61,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-64354-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"4 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}