{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:14:34Z","timestamp":1784837674444,"version":"3.55.0"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T00:00:00Z","timestamp":1484092800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["ICT12-059"],"award-info":[{"award-number":["ICT12-059"]}],"id":[{"id":"10.13039\/501100001821","id-type":"DOI","asserted-by":"publisher"}]}],"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-9402-4","type":"journal-article","created":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T18:46:28Z","timestamp":1484160388000},"page":"3-45","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":47,"title":["Complexity and Resource Bound Analysis of Imperative Programs Using Difference Constraints"],"prefix":"10.1007","volume":"59","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8922-0936","authenticated-orcid":false,"given":"Moritz","family":"Sinn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,1,11]]},"reference":[{"issue":"1","key":"9402_CR1","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":"9402_CR2","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: Cousot, R., Martel, M. (eds.) Static Analysis: 17th International Symposium, SAS 2010, Perpignan, France, September 14\u201316, 2010. Proceedings. Springer Berlin Heidelberg, Berlin (2010)","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"9402_CR3","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.ic.2012.03.003","volume":"215","author":"R Bagnara","year":"2012","unstructured":"Bagnara, R., Mesnard, F., Pescetti, A., Zaffanella, E.: A new look at the automatic synthesis of linear ranking functions. Inf. Comput. 215, 47\u201367 (2012)","journal-title":"Inf. Comput."},{"key":"9402_CR4","doi-asserted-by":"publisher","unstructured":"Ben-Amram, A.M.: Size-change termination with difference constraints. ACM Trans. Program. Lang. Syst. TOPLAS, 30(3), (2008). doi: 10.1145\/1353445.1353450","DOI":"10.1145\/1353445.1353450"},{"issue":"1","key":"9402_CR5","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/1180475.1180480","volume":"29","author":"AM Ben-Amram","year":"2007","unstructured":"Ben-Amram, A.M., Lee, C.S.: Program termination analysis in polynomial time. ACM Trans. Program. Lang. Syst. TOPLAS 29(1), 5 (2007)","journal-title":"ACM Trans. Program. Lang. Syst. TOPLAS"},{"issue":"4","key":"9402_CR6","doi-asserted-by":"publisher","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 Trans. Program. Lang. Syst. 38(4), 13:1\u201313:50 (2016)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9402_CR7","doi-asserted-by":"publisher","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: PLDI (2015)","DOI":"10.1145\/2737924.2737955"},{"key":"9402_CR8","doi-asserted-by":"publisher","unstructured":"Colcombet, T., Daviaud, L., Zuleger, F.: Size-change abstraction and max-plus automata. In: MFCS, pp. 208\u2013219 (2014)","DOI":"10.1007\/978-3-662-44522-8_18"},{"key":"9402_CR9","doi-asserted-by":"publisher","unstructured":"Coppa, E., Demetrescu, C., Finocchi, I.: Input-sensitive profiling. In: PLDI, pp. 89\u201398 (2012)","DOI":"10.1145\/2254064.2254076"},{"key":"9402_CR10","doi-asserted-by":"publisher","unstructured":"Flores-Montoya, A., H\u00e4hnle, R.: Resource analysis of complex programs with cost equations. In: APLAS, pp. 275\u2013295 (2014)","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"9402_CR11","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. In: PLDI, pp. 375\u2013385 (2009)","DOI":"10.1145\/1542476.1542518"},{"key":"9402_CR12","unstructured":"Gulwani, S., Juvekar, S.: Bound analysis using backward symbolic execution. Technical Report MSR-TR-2004-95, Microsoft Research (2009)"},{"key":"9402_CR13","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Lev-Ami, T., Sagiv, M.: A combination framework for tracking partition sizes. In: POPL, pp. 239\u2013251 (2009)","DOI":"10.1145\/1594834.1480912"},{"key":"9402_CR14","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.M.: Speed: precise and efficient static estimation of program computational complexity. In: POPL, pp. 127\u2013139 (2009)","DOI":"10.1145\/1594834.1480898"},{"key":"9402_CR15","doi-asserted-by":"publisher","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292\u2013304 (2010)","DOI":"10.1145\/1806596.1806630"},{"issue":"3","key":"9402_CR16","doi-asserted-by":"publisher","first-page":"14","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 (2012)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"9402_CR17","unstructured":"http:\/\/ctuning.org\/wiki\/index.php\/CTools:CBench"},{"key":"9402_CR18","unstructured":"http:\/\/forsyte.at\/software\/loopus\/"},{"key":"9402_CR19","unstructured":"http:\/\/forsyte.at\/static\/people\/sinn\/loopusJAR\/"},{"key":"9402_CR20","unstructured":"https:\/\/github.com\/s-falke\/llvm2kittel"},{"key":"9402_CR21","unstructured":"https:\/\/www.spec.org\/cpu2006\/"},{"key":"9402_CR22","doi-asserted-by":"publisher","unstructured":"Jin, G., Song, L., Shi, X., Scherpelz, J., Lu, S.: Understanding and detecting real-world performance bugs. In: PLDI, pp. 77\u201388 (2012)","DOI":"10.1145\/2254064.2254075"},{"key":"9402_CR23","doi-asserted-by":"publisher","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis and transformation. In: CGO, pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"9402_CR24","doi-asserted-by":"publisher","unstructured":"Magill, S., Tsai, M.-H., Lee, P., Tsay, Y.-K.: Automatic numeric abstractions for heap-manipulating programs. In: POPL, pp. 211\u2013222 (2010)","DOI":"10.1145\/1706299.1706326"},{"key":"9402_CR25","doi-asserted-by":"publisher","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: VMCAI, pp. 239\u2013251 (2004)","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"9402_CR26","doi-asserted-by":"crossref","unstructured":"Seidl, H., Gawlitza T.M., Schwarz, M.: Parametric strategy iteration. In: Kutsia, T., Voronkov, A. (eds.) SCSS 2014. 6th International Symposium on Symbolic Computation in Software Science, Volume 30 of EPiC Series in Computing, pp. 62\u201376. EasyChair (2014)","DOI":"10.29007\/c4kg"},{"key":"9402_CR27","doi-asserted-by":"crossref","unstructured":"Sinn, M., Zuleger, F., Veith, H.: Difference constraints: an adequate abstraction for complexity analysis of imperative programs. In: FMCAD, pp. 144\u2013151 (2015)","DOI":"10.1109\/FMCAD.2015.7542264"},{"key":"9402_CR28","doi-asserted-by":"crossref","unstructured":"Sinn, M., Zuleger, F., Veith, H.: A simple and scalable static analysis for bound analysis and amortized complexity analysis. CoRR, abs\/1401.5842 (2014)","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"9402_CR29","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: CAV, pp. 745\u2013761. Springer (2014)","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"9402_CR30","unstructured":"Sinn, M.: Automated complexity analysis for imperative programs. Ph.D. thesis, TU Wien, Faculty of Informatics, Wien (2016)"},{"key":"9402_CR31","doi-asserted-by":"publisher","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: FOSSACS, pp. 288\u2013302 (2009)","DOI":"10.1007\/978-3-642-00596-1_21"},{"issue":"2","key":"9402_CR32","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1137\/0606031","volume":"6","author":"RE Tarjan","year":"1985","unstructured":"Tarjan, R.E.: Amortized computational complexity. SIAM J. Algebraic Discrete Methods 6(2), 306\u2013318 (1985)","journal-title":"SIAM J. Algebraic Discrete Methods"},{"issue":"3","key":"9402_CR33","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/1347375.1347389","volume":"7","author":"R Wilhelm","year":"2008","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenstr\u00f6m, P.: The worst-case execution-time problem\u2014overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. 7(3), 36 (2008). doi: 10.1145\/1347375.1347389","journal-title":"ACM Trans. Embed. Comput. Syst."},{"key":"9402_CR34","doi-asserted-by":"publisher","unstructured":"Zaparanuks, D., Hauswirth, M.: Algorithmic profiling. In: PLDI, pp. 67\u201376 (2012)","DOI":"10.1145\/2254064.2254074"},{"key":"9402_CR35","doi-asserted-by":"publisher","unstructured":"Zuleger, F., Gulwani, S., Sinn, M., Veith, H.: Bound analysis of imperative programs with the size-change abstraction. In: SAS, pp. 280\u2013297 (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-9402-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9402-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-016-9402-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T09:40:57Z","timestamp":1749894057000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-016-9402-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,11]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["9402"],"URL":"https:\/\/doi.org\/10.1007\/s10817-016-9402-4","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,1,11]]}}}