{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T22:22:44Z","timestamp":1784240564003,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642237010","type":"print"},{"value":"9783642237027","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23702-7_22","type":"book-chapter","created":{"date-parts":[[2011,9,9]],"date-time":"2011-09-09T17:31:31Z","timestamp":1315589491000},"page":"280-297","source":"Crossref","is-referenced-by-count":66,"title":["Bound Analysis of Imperative Programs with the Size-Change Abstraction"],"prefix":"10.1007","author":[{"given":"Florian","family":"Zuleger","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sumit","family":"Gulwani","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Moritz","family":"Sinn","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helmut","family":"Veith","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"22_CR1","unstructured":"http:\/\/ctuning.org\/wiki\/index.php\/CTools:CBench"},{"key":"22_CR2","unstructured":"http:\/\/www.mrtc.mdh.se\/projects\/wcet\/benchmarks.html"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M.: Monotonicity constraints for termination in the integer domain. Technical report (2011)","DOI":"10.2168\/LMCS-7(3:4)2011"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Variance analyses from invariance analyses. In: POPL, pp. 211\u2013224 (2007)","DOI":"10.1145\/1190215.1190249"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Beyer, D., Cimatti, A., Griggio, A., Keremoglu, M.E., Sebastiani, R.: Software model checking via large-block encoding. In: FMCAD, pp. 25\u201332 (2009)","DOI":"10.1109\/FMCAD.2009.5351147"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Colby, C., Lee, P.: Trace-based program analysis. In: POPL, pp. 195\u2013207 (1996)","DOI":"10.1145\/237721.237776"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426 (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"22_CR8","unstructured":"Dutertre, B., de Moura, L.: The yices smt solver. Technical report (2006)"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Goldsmith, S., Aiken, A., Wilkerson, D.S.: Measuring empirical computational complexity. In: ESEC\/SIGSOFT FSE, pp. 395\u2013404 (2007)","DOI":"10.1145\/1287624.1287681"},{"key":"22_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/11817963_41","volume-title":"Computer Aided Verification","author":"D. Gopan","year":"2006","unstructured":"Gopan, D., Reps, T.W.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 452\u2013466. Springer, Heidelberg (2006)"},{"key":"22_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-540-70545-1_35","volume-title":"Computer Aided Verification","author":"B.S. Gulavani","year":"2008","unstructured":"Gulavani, B.S., Gulwani, S.: A numerical abstract domain based on expression abstraction and max operator with application in timing analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 370\u2013384. Springer, Heidelberg (2008)"},{"key":"22_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-642-02658-4_7","volume-title":"Computer Aided Verification","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S.: SPEED: Symbolic complexity bound analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 51\u201362. Springer, Heidelberg (2009)"},{"key":"22_CR13","doi-asserted-by":"crossref","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":"22_CR14","doi-asserted-by":"crossref","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":"22_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. In: PLDI, pp. 292\u2013304 (2010)","DOI":"10.1145\/1806596.1806630"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/978-3-642-15769-1_4","volume-title":"Static Analysis","author":"M. Heizmann","year":"2010","unstructured":"Heizmann, M., Jones, N.D., Podelski, A.: Size-change termination and transition invariants. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 22\u201350. Springer, Heidelberg (2010)"},{"key":"22_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-3-540-73595-3_34","volume-title":"Automated Deduction \u2013 CADE-21","author":"A. Krauss","year":"2007","unstructured":"Krauss, A.: Certified size-change termination. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 460\u2013475. Springer, Heidelberg (2007)"},{"key":"22_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-642-14295-6_9","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2010","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 89\u2013103. Springer, Heidelberg (2010)"},{"key":"22_CR19","volume-title":"CGO 2004: Proceedings of the International Symposium on Code Generation and Optimization","author":"C. Lattner","year":"2004","unstructured":"Lattner, C., Adve, V.: Llvm: A compilation framework for lifelong program analysis & transformation. In: CGO 2004: Proceedings of the International Symposium on Code Generation and Optimization, p. 75. IEEE Computer Society, Washington, DC, USA (2004)"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81\u201392 (2001)","DOI":"10.1145\/360204.360210"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1007\/11817963_36","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"2006","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 401\u2013414. Springer, Heidelberg (2006)"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Automatic modular abstractions for linear constraints. In: POPL, pp. 140\u2013151 (2009)","DOI":"10.1145\/1594834.1480899"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: POPL, pp. 132\u2013144 (2005)","DOI":"10.1145\/1040305.1040317"},{"key":"22_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/978-3-540-77505-8_26","volume-title":"Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues","author":"C. Popeea","year":"2008","unstructured":"Popeea, C., Chin, W.-N.: Inferring disjunctive postconditions. In: Okada, M., Satoh, I. (eds.) ASIAN 2006. LNCS, vol.\u00a04435, pp. 331\u2013345. Springer, Heidelberg (2008)"},{"key":"22_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-19835-9_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Tsitovich","year":"2011","unstructured":"Tsitovich, A., Sharygina, N., Wintersteiger, C.M., Kroening, D.: Loop summarization and termination analysis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 81\u201395. Springer, Heidelberg (2011)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23702-7_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,15]],"date-time":"2019-06-15T03:03:27Z","timestamp":1560567807000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23702-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642237010","9783642237027"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23702-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}