{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:01Z","timestamp":1747592461740,"version":"3.37.3"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319668444"},{"type":"electronic","value":"9783319668451"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_6","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T15:37:20Z","timestamp":1503761840000},"page":"85-101","source":"Crossref","is-referenced-by-count":9,"title":["Complexity Analysis for Java with AProVE"],"prefix":"10.1007","author":[{"given":"Florian","family":"Frohn","sequence":"first","affiliation":[]},{"given":"J\u00fcrgen","family":"Giesl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"issue":"1","key":"6_CR1","doi-asserted-by":"crossref","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. Comp. Sci. 413(1), 142\u2013159 (2012)","journal-title":"Theor. Comp. Sci."},{"key":"6_CR2","unstructured":"AProVE. https:\/\/aprove-developers.github.io\/jbc-complexity\/"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"Atkey, R.: Amortised resource analysis with separation logic. Logical Methods Comput. Sci. 7(2) (2011)","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/978-3-662-49674-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Avanzini","year":"2016","unstructured":"Avanzini, M., Moser, G., Schaper, M.: TcT: Tyrolean complexity tool. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 407\u2013423. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_24"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1007\/978-3-642-17172-7_2","volume-title":"Verification, Induction, Termination Analysis","author":"M Brockschmidt","year":"2010","unstructured":"Brockschmidt, M., Otto, C., Essen, C., Giesl, J.: Termination graphs for Java Bytecode. In: Siegler, S., Wasser, N. (eds.) Verification, Induction, Termination Analysis. LNCS, vol. 6463, pp. 17\u201337. Springer, Heidelberg (2010). doi: 10.1007\/978-3-642-17172-7_2"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-642-31424-7_13","volume-title":"Computer Aided Verification","author":"M Brockschmidt","year":"2012","unstructured":"Brockschmidt, M., Musiol, R., Otto, C., Giesl, J.: Automated termination proofs for Java programs with cyclic data. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 105\u2013122. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-31424-7_13"},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-662-49674-9_22","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Cook, B., Ishtiaq, S., Khlaaf, H., Piterman, N.: T2: temporal property verification. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 387\u2013393. Springer, Heidelberg (2016). doi: 10.1007\/978-3-662-49674-9_22"},{"issue":"4","key":"6_CR8","doi-asserted-by":"crossref","first-page":"13:1","DOI":"10.1145\/2866575","volume":"38","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM TOPLAS 38(4), 13:1\u201313:50 (2016)","journal-title":"ACM TOPLAS"},{"key":"6_CR9","unstructured":"Complexity Analysis-Based Guaranteed Execution. http:\/\/www.draper.com\/news\/draper-s-cage-could-spot-code-vulnerable-denial-service-attacks"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Proceedings of the PLDI 2015, pp. 467\u2013478 (2015)","DOI":"10.1145\/2737924.2737955"},{"issue":"5","key":"6_CR11","doi-asserted-by":"crossref","first-page":"826","DOI":"10.1145\/161468.161472","volume":"15","author":"S Debray","year":"1993","unstructured":"Debray, S., Lin, N.-W.: Cost analysis of logic programs. ACM TOPLAS 15(5), 826\u2013875 (1993)","journal-title":"ACM TOPLAS"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-319-12736-1_15","volume-title":"Programming Languages and Systems","author":"A Flores-Montoya","year":"2014","unstructured":"Flores-Montoya, A., H\u00e4hnle, R.: Resource analysis of complex programs with cost equations. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 275\u2013295. Springer, Cham (2014). doi: 10.1007\/978-3-319-12736-1_15"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/3-540-47813-2_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Genaim","year":"2002","unstructured":"Genaim, S., Codish, M., Gallagher, J., Lagoon, V.: Combining norms to prove termination. In: Cortesi, A. (ed.) VMCAI 2002. LNCS, vol. 2294, pp. 126\u2013138. Springer, Heidelberg (2002). doi: 10.1007\/3-540-47813-2_9"},{"issue":"1","key":"6_CR14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10817-016-9388-y","volume":"58","author":"J Giesl","year":"2017","unstructured":"Giesl, J., Aschermann, C., Brockschmidt, M., Emmes, F., Frohn, F., Fuhs, C., Hensel, J., Otto, C., Pl\u00fccker, M., Schneider-Kamp, P., Str\u00f6der, T., Swiderski, S., Thiemann, R.: Analyzing program termination and complexity automatically with AProVE. J. Autom. Reasoning 58(1), 3\u201331 (2017)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: precise and efficient static estimation of program computational complexity. In: Proceedings of the POPL 2009, pp. 127\u2013139 (2009)","DOI":"10.1145\/1594834.1480898"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-51081-8_107","volume-title":"Rewriting Techniques and Applications","author":"D Hofbauer","year":"1989","unstructured":"Hofbauer, D., Lautemann, C.: Termination proofs and the length of derivations. In: Dershowitz, N. (ed.) RTA 1989. LNCS, vol. 355, pp. 167\u2013177. Springer, Heidelberg (1989). doi: 10.1007\/3-540-51081-8_107"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Hoffmann, J., Das, A., Weng, S.-C.: Towards automatic resource bound analysis for OCaml. In: Proceedings of the POPL 2017, pp. 359\u2013373 (2017)","DOI":"10.1145\/3009837.3009842"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"593","DOI":"10.1007\/978-3-642-37036-6_32","volume-title":"Programming Languages and Systems","author":"M Hofmann","year":"2013","unstructured":"Hofmann, M., Rodriguez, D.: Automatic type inference for amortised heap-space analysis. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 593\u2013613. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-37036-6_32"},{"key":"6_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-40561-7_20","volume-title":"Software Engineering and Formal Methods","author":"R Ji","year":"2013","unstructured":"Ji, R., H\u00e4hnle, R., Bubel, R.: Program transformation based on symbolic execution and deduction. In: Hierons, R.M., Merayo, M.G., Bravetti, M. (eds.) SEFM 2013. LNCS, vol. 8137, pp. 289\u2013304. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40561-7_20"},{"issue":"4","key":"6_CR20","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM TOPLAS 28(4), 619\u2013695 (2006)","journal-title":"ACM TOPLAS"},{"issue":"1","key":"6_CR21","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1007\/s10817-013-9277-6","volume":"51","author":"L Noschinski","year":"2013","unstructured":"Noschinski, L., Emmes, F., Giesl, J.: Analyzing innermost runtime complexity of term rewriting by dependency pairs. J. Autom. Reasoning 51(1), 27\u201356 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Proceedings of the RTA 2010, LIPIcs 6, pp. 259\u2013276 (2010)","DOI":"10.1007\/978-3-642-17172-7_2"},{"issue":"1","key":"6_CR23","doi-asserted-by":"crossref","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. Reasoning 59(1), 3\u201345 (2017)","journal-title":"J. Autom. Reasoning"},{"key":"6_CR24","unstructured":"Space\/Time Analysis for Cybersecurity (STAC). http:\/\/www.darpa.mil\/program\/space-time-analysis-for-cybersecurity"},{"issue":"3","key":"6_CR25","first-page":"36:1","volume":"7","author":"R Wilhelm","year":"2008","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenstr\u00f6m, P.: The worst-case execution-time problem - overview of methods and survey of tools. ACM TECS 7(3), 36:1\u201336:53 (2008)","journal-title":"ACM TECS"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T20:25:45Z","timestamp":1659385545000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}