{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:09Z","timestamp":1740123369355,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2016,12,17]],"date-time":"2016-12-17T00:00:00Z","timestamp":1481932800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"Seventh Framework Programme (BE)","award":["FP7-ICT-610582","FP7-ICT-610582"],"award-info":[{"award-number":["FP7-ICT-610582","FP7-ICT-610582"]}]},{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"publisher","award":["TIN2012-38137","TIN2012-38137"],"award-info":[{"award-number":["TIN2012-38137","TIN2012-38137"]}],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"publisher","award":["TIN2015-69175-C4-2-R","TIN2015-69175-C4-2-R"],"award-info":[{"award-number":["TIN2015-69175-C4-2-R","TIN2015-69175-C4-2-R"]}],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"publisher"}]},{"name":"Comunidad de Madrid (ES)","award":["S2013\/ICE-3006","S2013\/ICE-3006"],"award-info":[{"award-number":["S2013\/ICE-3006","S2013\/ICE-3006"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10817-016-9400-6","type":"journal-article","created":{"date-parts":[[2016,12,17]],"date-time":"2016-12-17T11:58:30Z","timestamp":1481975910000},"page":"47-85","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Rely-Guarantee Termination and Cost Analyses of Loops with Concurrent Interleavings"],"prefix":"10.1007","volume":"59","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Antonio","family":"Flores-Montoya","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1664-018X","authenticated-orcid":false,"given":"Enrique","family":"Martin-Martin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,12,17]]},"reference":[{"key":"9400_CR1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"Actors: A Model of Concurrent Computation in Distributed Systems","author":"G Agha","year":"1986","unstructured":"Agha, G.: Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge (1986)"},{"issue":"3","key":"9400_CR2","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1002\/stvr.1569","volume":"25","author":"E Albert","year":"2015","unstructured":"Albert, E., Arenas, P., Correas, J., Genaim, S., G\u00f3mez-Zamalloa, M., Rom\u00e1n-D\u00edez, G.P., Puebla, G.: Object-sensitive cost analysis for concurrent objects. Softw. Test. Verif. Reliab. 25(3), 218\u2013271 (2015). doi: 10.1002\/stvr.1569","journal-title":"Softw. Test. Verif. Reliab."},{"key":"9400_CR3","doi-asserted-by":"publisher","unstructured":"Albert, E., Arenas, P., Flores-Montoya, A., Genaim, S., G\u00f3mez-Zamalloa, M., Martin-Martin, E., Puebla, G., Rom\u00e1n-D\u00edez, G.: SACO: Static analyzer for concurrent objects. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) Tools and Algorithms for the Construction and Analysis of Systems\u201420th International Conference, TACAS 2014. Lecture Notes in Computer Science, vol. 8413, pp. 562\u2013567. Springer (2014). doi: 10.1007\/978-3-642-54862-8_46","DOI":"10.1007\/978-3-642-54862-8_46"},{"key":"9400_CR4","doi-asserted-by":"publisher","unstructured":"Albert, E., Arenas, P., Genaim, S., G\u00f3mez-Zamalloa, M., Puebla, G.: Cost analysis of concurrent OO programs. In: Yang, H. (ed.) Programming Languages and Systems-9th Asian Symposium, APLAS 2011, Kenting, Taiwan, December 5\u20137, 2011. Proceedings, Lecture Notes in Computer Science, vol. 7078, pp. 238\u2013254. Springer (2011). doi: 10.1007\/978-3-642-25318-8_19","DOI":"10.1007\/978-3-642-25318-8_19"},{"issue":"2","key":"9400_CR5","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/s10817-010-9174-1","volume":"46","author":"E Albert","year":"2011","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-form upper bounds in static cost analysis. J. Autom. Reason. 46(2), 161\u2013203 (2011). doi: 10.1007\/s10817-010-9174-1","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9400_CR6","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1016\/j.scico.2014.12.001","volume":"111","author":"E Albert","year":"2015","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G.: A practical comparator of cost functions and its applications. Sci. Comput. Progr. 111(3), 483\u2013504 (2015). doi: 10.1016\/j.scico.2014.12.001","journal-title":"Sci. Comput. Progr."},{"key":"9400_CR7","doi-asserted-by":"publisher","unstructured":"Albert, E., Correas, J., Johnsen, E.B., Rom\u00e1n-D\u00edez, G.: Parallel cost analysis of distributed systems. In: Static Analysis-22nd International Symposium, SAS 2015. Proceedings, Lecture Notes in Computer Science, vol. 9291, pp. 275\u2013292. Springer (2015). doi: 10.1007\/978-3-662-48288-9_16","DOI":"10.1007\/978-3-662-48288-9_16"},{"issue":"4","key":"9400_CR8","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1007\/s00165-014-0321-z","volume":"27","author":"E Albert","year":"2015","unstructured":"Albert, E., Correas, J., Puebla, G., Rom\u00e1n-D\u00edez, G.: Quantified abstract configurations of distributed systems. Form. Asp. Comput. 27(4), 665\u2013699 (2015). doi: 10.1007\/s00165-014-0321-z","journal-title":"Form. Asp. Comput."},{"key":"9400_CR9","doi-asserted-by":"publisher","unstructured":"Albert, E., Correas, J., Rom\u00e1n-D\u00edez, G.: Non-cumulative resource analysis. In: Proceedings of 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2015). Lecture Notes in Computer Science, vol. 9035, pp. 85\u2013100. Springer (2015). doi: 10.1007\/978-3-662-46681-0_6","DOI":"10.1007\/978-3-662-46681-0_6"},{"key":"9400_CR10","doi-asserted-by":"publisher","unstructured":"Albert, E., Flores-Montoya, A., Genaim, S.: Analysis of may-happen-in-parallel in concurrent objects. In: Giese, H., Rosu, G. (eds.) Formal Techniques for Distributed Systems-Joint 14th IFIP WG 6.1 International Conference, FMOODS 2012 and 32nd IFIP WG 6.1 International Conference, FORTE 2012, Stockholm, Sweden, June 13\u201316, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7273, pp. 35\u201351. Springer (2012). doi: 10.1007\/978-3-642-30793-5_3","DOI":"10.1007\/978-3-642-30793-5_3"},{"key":"9400_CR11","doi-asserted-by":"publisher","unstructured":"Albert, E., Flores-Montoya, A., Genaim, S., Martin-Martin, E.: Termination and cost analysis of loops with concurrent interleavings. In: Hung, D.V., Ogawa, M. (eds.) Automated Technology for Verification and Analysis-11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15\u201318, 2013. Proceedings, Lecture Notes in Computer Science, vol. 8172, pp. 349\u2013364. Springer (2013). doi: 10.1007\/978-3-319-02444-8_25","DOI":"10.1007\/978-3-319-02444-8_25"},{"key":"9400_CR12","doi-asserted-by":"publisher","unstructured":"Albert, E., Genaim, S., Gordillo, P.: May-happen-in-parallel analysis for asynchronous programs with inter-procedural synchronization. In: Static Analysis-22nd International Symposium, SAS 2015. Proceedings, Lecture Notes in Computer Science, vol. 9291, pp. 72\u201389. Springer (2015). doi: 10.1007\/978-3-662-48288-9_5","DOI":"10.1007\/978-3-662-48288-9_5"},{"key":"9400_CR13","doi-asserted-by":"publisher","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Isabel, M.: Combining static analysis and testing for deadlock detection. In: Integrated Formal Methods-12th International Conference, IFM 2016, Reykjavik, Iceland, June 1\u20135, 2016. Proceedings, Lecture Notes in Computer Science, vol. 9681, pp. 409\u2013424. Springer (2016)","DOI":"10.1007\/978-3-319-33693-0_26"},{"key":"9400_CR14","doi-asserted-by":"publisher","unstructured":"Albert, E., G\u00f3mez-Zamalloa, M., Isabel, M.: Syco: A systematic testing tool for concurrent objects. In: Zaks, A., Hermenegildo, M.V. (eds.) Proceedings of the 25th International Conference on Compiler Construction, CC 2016, Barcelona, Spain, March 12\u201318 2016, pp. 269\u2013270. ACM (2016)","DOI":"10.1145\/2892208.2892236"},{"key":"9400_CR15","doi-asserted-by":"publisher","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Proceedings of the SAS\u201910, LNCS, vol. 6337, pp. 117\u2013133. Springer (2010)","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"9400_CR16","volume-title":"Concurrent Programming in Erlang","author":"J Armstrong","year":"1996","unstructured":"Armstrong, J., Virding, R., Wistrom, C., Williams, M.: Concurrent Programming in Erlang. Prentice Hall, Upper Saddle River (1996)"},{"key":"9400_CR17","doi-asserted-by":"publisher","unstructured":"Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Alternating runtime and size complexity analysis of integer programs. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2014). Lecture Notes in Computer Science, vol. 8413, pp. 140\u2013155. Springer (2014)","DOI":"10.1007\/978-3-642-54862-8_10"},{"key":"9400_CR18","doi-asserted-by":"publisher","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 467\u2013478. ACM, New York (2015). doi: 10.1145\/2737924.2737955","DOI":"10.1145\/2737924.2737955"},{"key":"9400_CR19","doi-asserted-by":"publisher","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving thread termination. In: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI \u201907, pp. 320\u2013330. ACM, New York (2007). doi: 10.1145\/1250734.1250771","DOI":"10.1145\/1250734.1250771"},{"issue":"5","key":"9400_CR20","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1145\/1941487.1941509","volume":"54","author":"B Cook","year":"2011","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun. ACM 54(5), 88\u201398 (2011)","journal-title":"Commun. ACM"},{"key":"9400_CR21","doi-asserted-by":"publisher","unstructured":"de\u00a0Boer, F.S., Clarke, D., Johnsen, E.B.: A complete guide to the future. In: de\u00a0Nicola, R. (ed.) Programming Languages and Systems, 16th European Symposium on Programming, ESOP 2007, Held as Part of the Joint European Conferences on Theory and Practics of Software, ETAPS 2007, Braga, Portugal, March 24\u2013April 1, 2007. Proceedings, Lecture Notes in Computer Science, vol. 4421, pp. 316\u2013330. Springer (2007)","DOI":"10.1007\/978-3-540-71316-6_22"},{"key":"9400_CR22","doi-asserted-by":"publisher","unstructured":"Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: ESOP, Lecture Notes in Computer Science, vol. 2305, pp. 262\u2013277. Springer (2002)","DOI":"10.1007\/3-540-45927-8_19"},{"key":"9400_CR23","doi-asserted-by":"publisher","unstructured":"Flores-Montoya, A., H\u00e4hnle, R.: Resource analysis of complex programs with cost equations. In: Programming Languages and Systems-12th Asian Symposium, APLAS 2014, Singapore, November 17\u201319, 2014. Proceedings, LNCS, vol. 8858, pp. 275\u2013295. Springer (2014)","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"9400_CR24","doi-asserted-by":"publisher","unstructured":"Garcia, A., Laneve, C., Lienhardt, M.: Static analysis of cloud elasticity. In: Falaschi, M., Albert, E. (eds.) Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14\u201316, 2015, pp. 125\u2013136. ACM (2015). doi: 10.1145\/2790449.2790524","DOI":"10.1145\/2790449.2790524"},{"key":"9400_CR25","doi-asserted-by":"publisher","unstructured":"Gotsman, A., Cook, B., Parkinson, M.J., Vafeiadis, V.: Proving that non-blocking algorithms don\u2019t block. In: Shao, Z., Pierce, B.C. (eds.) Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 16\u201328. ACM (2009). doi: 10.1145\/1480881.1480886","DOI":"10.1145\/1480881.1480886"},{"issue":"2\u20133","key":"9400_CR26","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1016\/j.tcs.2008.09.019","volume":"410","author":"P Haller","year":"2009","unstructured":"Haller, P., Odersky, M.: Scala actors: unifying thread-based and event-based programming. Theor. Comput. Sci. 410(2\u20133), 202\u2013220 (2009). doi: 10.1016\/j.tcs.2008.09.019","journal-title":"Theor. Comput. Sci."},{"key":"9400_CR27","doi-asserted-by":"crossref","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.C., de\u00a0Boer, F.S., Bonsangue, M.M. (eds.) Formal Methods for Components and Objects-9th International Symposium, FMCO 2010, Graz, Austria, November 29\u2013December 1, 2010. Revised Papers, Lecture Notes in Computer Science, vol. 6957, pp. 142\u2013164. Springer (2012)","DOI":"10.1007\/978-3-642-25271-6_8"},{"key":"9400_CR28","doi-asserted-by":"publisher","unstructured":"Kupriyanov, A., Finkbeiner, B.: Causal termination of multi-threaded programs. In: Biere, A., Bloem, R. (eds.) 26th International Conference on Computer Aided Verification (CAV 2014). Lecture Notes in Computer Science, vol. 8559, pp. 814\u2013830. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_54"},{"key":"9400_CR29","doi-asserted-by":"publisher","unstructured":"Popeea, C., Rybalchenko, A.: Compositional termination proofs for multi-threaded programs. In: Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS\u201912, pp. 237\u2013251. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_17","DOI":"10.1007\/978-3-642-28756-5_17"},{"key":"9400_CR30","doi-asserted-by":"publisher","unstructured":"Sch\u00e4fer, J., Poetzsch-Heffter, A.: JCobox: Generalizing active objects to concurrent components. In: D\u2019Hondt, T. (ed.) ECOOP 2010-Object-Oriented Programming, 24th European Conference, Maribor, Slovenia, June 21\u201325, 2010. Proceedings, LNCS, vol. 6183, pp. 275\u2013299. Springer (2010)","DOI":"10.1007\/978-3-642-14107-2_13"},{"key":"9400_CR31","doi-asserted-by":"publisher","unstructured":"Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Proceeding of Computer Aided Verification 2014, vol. 8559, pp. 745\u2013761. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"9400_CR32","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Difference constraints: an adequate abstraction for complexity analysis of imperative programs. CoRR abs\/1508.04958 (2015). http:\/\/arxiv.org\/abs\/1508.04958"},{"key":"9400_CR33","doi-asserted-by":"publisher","unstructured":"Srinivasan, S., Mycroft, A.: Kilim: Isolation-typed actors for Java. In: Vitek, J. (ed.) ECOOP 2008-Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7\u201311, 2008. Proceedings, Lecture Notes in Computer Science, vol. 5142, pp. 104\u2013128. Springer (2008)","DOI":"10.1007\/978-3-540-70592-5_6"},{"key":"9400_CR34","doi-asserted-by":"publisher","unstructured":"Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: Yahav, E. (ed.) SAS, Lecture Notes in Computer Science, vol. 6887, pp. 280\u2013297. Springer (2011)","DOI":"10.1007\/978-3-642-23702-7_22"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-016-9400-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9400-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9400-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,28]],"date-time":"2020-09-28T01:22:26Z","timestamp":1601256146000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9400-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,17]]},"references-count":34,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["9400"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9400-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2016,12,17]]}}}