{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:01:34Z","timestamp":1760043694543},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319402284"},{"type":"electronic","value":"9783319402291"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-40229-1_37","type":"book-chapter","created":{"date-parts":[[2016,6,11]],"date-time":"2016-06-11T12:54:04Z","timestamp":1465649644000},"page":"550-567","source":"Crossref","is-referenced-by-count":20,"title":["Lower Runtime Bounds for Integer Programs"],"prefix":"10.1007","author":[{"given":"F.","family":"Frohn","sequence":"first","affiliation":[]},{"given":"M.","family":"Naaf","sequence":"additional","affiliation":[]},{"given":"J.","family":"Hensel","sequence":"additional","affiliation":[]},{"given":"M.","family":"Brockschmidt","sequence":"additional","affiliation":[]},{"given":"J.","family":"Giesl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,6,12]]},"reference":[{"issue":"3","key":"37_CR1","doi-asserted-by":"crossref","first-page":"22:1","DOI":"10.1145\/2499937.2499943","volume":"14","author":"E Albert","year":"2013","unstructured":"Albert, E., Genaim, S., Masud, A.N.: On the inference of resource usage upper and lower bounds. ACM Trans. Comput. Logic 14(3), 22:1\u201322:35 (2013)","journal-title":"ACM Trans. Comput. Logic"},{"key":"37_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/978-3-642-15769-1_8","volume-title":"Static Analysis","author":"C Alias","year":"2010","unstructured":"Alias, C., Darte, A., Feautrier, P., Gonnord, L.: Multi-dimensional rankings, program termination, and complexity bounds of flowchart programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 117\u2013133. Springer, Heidelberg (2010)"},{"key":"37_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"405","DOI":"10.1007\/978-3-642-33125-1_27","volume-title":"Static Analysis","author":"DE Alonso-Blas","year":"2012","unstructured":"Alonso-Blas, D.E., Genaim, S.: On the limits of the classical approach to cost analysis. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol. 7460, pp. 405\u2013421. Springer, Heidelberg (2012)"},{"key":"37_CR4","unstructured":"Bagnara, R., Pescetti, A., Zaccagnini, A., Zaffanella, E.: $${\\sf PURRS}$$ : towards computer algebra support for fully automatic worst-case complexity analysis. CoRR abs\/cs\/0512056 (2005)"},{"key":"37_CR5","unstructured":"Benchmark examples. https:\/\/github.com\/s-falke\/kittel-koat\/tree\/master\/koat-evaluation\/examples"},{"key":"37_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"37_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"413","DOI":"10.1007\/978-3-642-39799-8_28","volume-title":"Computer Aided Verification","author":"M Brockschmidt","year":"2013","unstructured":"Brockschmidt, M., Cook, B., Fuhs, C.: Better termination proving through cooperation. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 413\u2013429. Springer, Heidelberg (2013)"},{"key":"37_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1007\/978-3-642-54862-8_10","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Brockschmidt","year":"2014","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.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 140\u2013155. Springer, Heidelberg (2014)"},{"key":"37_CR9","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Grove, D., Blackburn, S. (eds.) PLDI 2015, pp. 467\u2013478, ACM (2015)","DOI":"10.1145\/2813885.2737955"},{"key":"37_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: $$\\sf Z3$$ : an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"37_CR11","unstructured":"Debray, S., L\u00f3pez-Garc\u00eda, P., Hermenegildo, M.V., Lin, N.: Lower bound cost estimation for logic programs. In: Maluszynski, J. (ed.) ILPS 1997, pp. 291\u2013305. MIT Press (1997)"},{"key":"37_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/978-3-642-27705-4_21","volume-title":"Verified Software: Theories, Tools, Experiments","author":"S Falke","year":"2012","unstructured":"Falke, S., Kapur, D., Sinz, C.: Termination analysis of imperative programs using bitvector arithmetic. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 261\u2013277. Springer, Heidelberg (2012)"},{"key":"37_CR13","doi-asserted-by":"crossref","unstructured":"Farzan, A., Kincaid, Z.: Compositional recurrence analysis. In: Kaivola, R., Wahl, T. (eds.) FMCAD 2015, pp. 57\u201364. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"37_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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, Heidelberg (2014)"},{"key":"37_CR15","unstructured":"Frohn, F., Giesl, J., Emmes, F., Str\u00f6der, T., Aschermann, C., Hensel, J.: Inferring lower bounds for runtime complexity. In: Fern\u00e1ndez, M. (ed.) RTA 2015. LIPIcs, vol. 36, pp. 334\u2013349. Dagstuhl Publishing (2015)"},{"key":"37_CR16","unstructured":"Frohn, F., Naaf, M., Hensel, J., Brockschmidt, M., Giesl, J.: Proofs and empirical evaluation of \u201cLower Runtime Bounds for Integer Programs\u201d (2016). http:\/\/aprove.informatik.rwth-aachen.de\/eval\/integerLower\/"},{"key":"37_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"144","DOI":"10.1007\/11823230_10","volume-title":"Static Analysis","author":"L Gonnord","year":"2006","unstructured":"Gonnord, L., Halbwachs, N.: Combining widening and acceleration in linear relation analysis. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 144\u2013160. Springer, Heidelberg (2006)"},{"key":"37_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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.) Rewriting Techniques and Applications. LNCS, vol. 355, pp. 167\u2013177. Springer, Heidelberg (1989)"},{"issue":"3","key":"37_CR19","doi-asserted-by":"crossref","first-page":"14:1","DOI":"10.1145\/2362389.2362393","volume":"34","author":"J Hoffmann","year":"2012","unstructured":"Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate amortized resource analysis. ACM Trans. Program. Lang. Syst. 34(3), 14:1\u201314:62 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"37_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: $${\\sf APRON}$$ : a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661\u2013667. Springer, Heidelberg (2009)"},{"issue":"1","key":"37_CR21","doi-asserted-by":"crossref","first-page":"529","DOI":"10.1145\/2578855.2535843","volume":"49","author":"B Jeannet","year":"2014","unstructured":"Jeannet, B., Schrammel, P., Sankaranarayanan, S.: Abstract acceleration of general linear loops. ACM SIGPLAN Not. 49(1), 529\u2013540 (2014)","journal-title":"ACM SIGPLAN Not."},{"issue":"1","key":"37_CR22","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/s10703-015-0228-1","volume":"47","author":"D Kroening","year":"2015","unstructured":"Kroening, D., Lewis, M., Weissenbacher, G.: Under-approximating loops in C programs for fast counterexample detection. Form. Meth. Sys. Des. 47(1), 75\u201392 (2015)","journal-title":"Form. Meth. Sys. Des."},{"key":"37_CR23","unstructured":"$${\\sf LoAT}$$ . https:\/\/github.com\/aprove-developers\/LoAT"},{"key":"37_CR24","doi-asserted-by":"crossref","unstructured":"Madhukar, K., Wachter, B., Kroening, D., Lewis, M., Srivas, M.K.: Accelerating invariant generation. In: Kaivola, R., Wahl, T. (eds.) FMCAD 2015, pp. 105\u2013111. IEEE (2015)","DOI":"10.1109\/FMCAD.2015.7542259"},{"key":"37_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"37_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"745","DOI":"10.1007\/978-3-319-08867-9_50","volume-title":"Computer Aided Verification","author":"M Sinn","year":"2014","unstructured":"Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 745\u2013761. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40229-1_37","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,22]],"date-time":"2020-09-22T04:09:57Z","timestamp":1600747797000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40229-1_37"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319402284","9783319402291"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40229-1_37","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}