{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:15:47Z","timestamp":1743034547754,"version":"3.40.3"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031081651"},{"type":"electronic","value":"9783031081668"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-08166-8_2","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"19-37","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["When COSTA Met KeY: Verified Cost Bounds"],"prefix":"10.1007","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alicia","family":"Merayo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillermo","family":"Rom\u00e1n-D\u00edez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"562","DOI":"10.1007\/978-3-642-54862-8_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Albert","year":"2014","unstructured":"Albert, E., et al.: SACO: static analyzer for concurrent objects. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 562\u2013567. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_46"},{"issue":"2","key":"2_CR2","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)","journal-title":"J. Autom. Reason."},{"key":"2_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-71316-6_12","volume-title":"Programming Languages and Systems","author":"E Albert","year":"2007","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of Java bytecode. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 157\u2013172. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-71316-6_12"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-92188-2_5","volume-title":"Formal Methods for Components and Objects","author":"E Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: design and implementation of a cost and termination analyzer for Java bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 113\u2013132. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-92188-2_5"},{"issue":"1","key":"2_CR5","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/j.tcs.2011.07.009","volume":"413","author":"E Albert","year":"2012","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: Cost analysis of object-oriented bytecode programs. Theor. Comput. Sci. 413(1), 142\u2013159 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"2_CR6","doi-asserted-by":"crossref","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., Puebla, G., Rom\u00e1n-D\u00edez, G.: Verified resource guarantees using COSTA and key. In: Proceedings of the 2011 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2011, pp. 73\u201376. ACM (2011)","DOI":"10.1145\/1929501.1929513"},{"issue":"4","key":"2_CR7","doi-asserted-by":"publisher","first-page":"987","DOI":"10.1007\/s10270-015-0476-y","volume":"15","author":"E Albert","year":"2016","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., Puebla, G., Rom\u00e1n-D\u00edez, G.: A formal verification framework for static analysis - as well as its instantiation to the resource analyzer COSTA and formal verification tool key. Softw. Syst. Model. 15(4), 987\u20131012 (2016)","journal-title":"Softw. Syst. Model."},{"key":"2_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-642-28872-2_10","volume-title":"Fundamental Approaches to Software Engineering","author":"E Albert","year":"2012","unstructured":"Albert, E., Bubel, R., Genaim, S., H\u00e4hnle, R., Rom\u00e1n-D\u00edez, G.: Verified resource guarantees for heap manipulating programs. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 130\u2013145. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_10"},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper and lower bounds. ACM Trans. Comput. Log. 14(3), 22:1\u201322:35 (2013)","DOI":"10.1145\/2499937.2499943"},{"key":"2_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-030-71500-7_2","volume-title":"Fundamental Approaches to Software Engineering","author":"E Albert","year":"2021","unstructured":"Albert, E., H\u00e4hnle, R., Merayo, A., Steinh\u00f6fel, D.: Certified abstract cost analysis. In: FASE 2021. LNCS, vol. 12649, pp. 24\u201345. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_2"},{"key":"2_CR11","unstructured":"Avanzini, M., Sternagel, C., Thiemann, R.: Certification of complexity proofs using CeTA. In: 26th International Conference on Rewriting Techniques and Applications, RTA 2015. LIPIcs, vol. 36, pp. 23\u201339. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2015)"},{"key":"2_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69061-0","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. 4334. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69061-0"},{"key":"2_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-642-54108-7_15","volume-title":"Verified Software: Theories, Tools, Experiments","author":"S Blazy","year":"2014","unstructured":"Blazy, S., Maroneze, A., Pichardie, D.: Formal verification of loop bound estimation for WCET analysis. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 281\u2013303. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_15"},{"key":"2_CR14","doi-asserted-by":"crossref","unstructured":"Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38(4):13:1\u201313:50 (2016)","DOI":"10.1145\/2866575"},{"key":"2_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-319-63046-5_28","volume-title":"Automated Deduction \u2013 CADE 26","author":"M Brockschmidt","year":"2017","unstructured":"Brockschmidt, M., Joosten, S.J.C., Thiemann, R., Yamada, A.: Certifying safety and termination proofs for integer transition systems. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 454\u2013471. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_28"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end verification of stack-space bounds for C programs. In: ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 270\u2013281. ACM (2014)","DOI":"10.1145\/2666356.2594301"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-319-63390-9_4","volume-title":"Computer Aided Verification","author":"Q Carbonneaux","year":"2017","unstructured":"Carbonneaux, Q., Hoffmann, J., Reps, T., Shao, Z.: Automated resource analysis with coq proof objects. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 64\u201385. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_4"},{"key":"2_CR18","unstructured":"Coq Development Team: The Coq Proof Assistant Reference Manual - Version 8.7 (2018)"},{"key":"2_CR19","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"},{"key":"2_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"254","DOI":"10.1007\/978-3-319-48989-6_16","volume-title":"FM 2016: Formal Methods","author":"A Flores-Montoya","year":"2016","unstructured":"Flores-Montoya, A.: Upper and lower amortized cost bounds of programs expressed as cost relations. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 254\u2013273. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_16"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-66845-1_6","volume-title":"Integrated Formal Methods","author":"F Frohn","year":"2017","unstructured":"Frohn, F., Giesl, J.: Complexity analysis for Java with AProVE. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 85\u2013101. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_6"},{"key":"2_CR22","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1\u201314:62 (2012)","DOI":"10.1145\/2362389.2362393"},{"key":"2_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-662-46669-8_6","volume-title":"Programming Languages and Systems","author":"J Hoffmann","year":"2015","unstructured":"Hoffmann, J., Shao, Z.: Automatic static cost analysis for parallel programs. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 132\u2013157. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_6"},{"key":"2_CR24","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":"7","key":"2_CR25","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"2_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-72016-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Meyer","year":"2021","unstructured":"Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. In: TACAS 2021. LNCS, vol. 12651, pp. 250\u2013269. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_14"},{"key":"2_CR27","doi-asserted-by":"crossref","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 496\u2013512. ACM (2018)","DOI":"10.1145\/3192366.3192394"},{"key":"2_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL - A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL - A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"1","key":"2_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10817-016-9402-4","volume":"59","author":"M Sinn","year":"2017","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Complexity and resource bound analysis of imperative programs using difference constraints. J. Autom. Reason. 59(1), 3\u201345 (2017)","journal-title":"J. Autom. Reason."},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyzer for java bytecode based on path-length. ACM Trans. Program. Lang. Syst. 32(3), 8:1\u20138:70 (2010)","DOI":"10.1145\/1709093.1709095"},{"key":"2_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-030-30942-8_20","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"D Steinh\u00f6fel","year":"2019","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: Abstract execution. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 319\u2013336. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_20"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452\u2013468. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_31"},{"issue":"9","key":"2_CR33","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1145\/361002.361016","volume":"18","author":"B Wegbreit","year":"1975","unstructured":"Wegbreit, B.: Mechanical program analysis. Commun. ACM 18(9), 528\u2013539 (1975)","journal-title":"Commun. ACM"}],"container-title":["Lecture Notes in Computer Science","The Logic of Software. A Tasting Menu of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-08166-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:38:09Z","timestamp":1656891489000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08166-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081651","9783031081668"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08166-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"4 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}