{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,28]],"date-time":"2026-04-28T03:47:30Z","timestamp":1777348050526,"version":"3.51.4"},"publisher-location":"Cham","reference-count":25,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319024431","type":"print"},{"value":"9783319024448","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-319-02444-8_26","type":"book-chapter","created":{"date-parts":[[2013,8,29]],"date-time":"2013-08-29T05:11:21Z","timestamp":1377753081000},"page":"365-380","source":"Crossref","is-referenced-by-count":37,"title":["Linear Ranking for Linear Lasso Programs"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Heizmann","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Leike","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"26_CR1","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. Reasoning\u00a046(2), 161\u2013203 (2011)","journal-title":"J. Autom. Reasoning"},{"key":"26_CR2","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.\u00a0215, 47\u201367 (2012)","journal-title":"Inf. Comput."},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops. In: POPL (2013)","DOI":"10.1145\/2429069.2429078"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-27940-9_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.M. Ben-Amram","year":"2012","unstructured":"Ben-Amram, A.M., Genaim, S., Masud, A.N.: On the termination of integer loops. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 72\u201387. Springer, Heidelberg (2012)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/11513988_48","volume-title":"Computer Aided Verification","author":"A.R. 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.\u00a03576, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"26_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1349","DOI":"10.1007\/11523468_109","volume-title":"Automata, Languages and Programming","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1349\u20131361. Springer, Heidelberg (2005)"},{"key":"26_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/11539452_37","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination analysis of integer linear loops. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 488\u2013502. Springer, Heidelberg (2005)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/11817963_34","volume-title":"Computer Aided Verification","author":"M. Braverman","year":"2006","unstructured":"Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 372\u2013385. Springer, Heidelberg (2006)"},{"key":"26_CR9","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.\u00a07358, pp. 105\u2013122. Springer, Heidelberg (2012)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/3-540-45319-9_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.A. Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"26_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-18275-4_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B. Cook","year":"2011","unstructured":"Cook, B., Fisher, J., Krepska, E., Piterman, N.: Proving stabilization of biological systems. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 134\u2013149. Springer, Heidelberg (2011)"},{"issue":"1","key":"26_CR12","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10703-013-0186-4","volume":"43","author":"B. Cook","year":"2013","unstructured":"Cook, B., Kroening, D., R\u00fcmmer, P., Wintersteiger, C.M.: Ranking function synthesis for bit-vector relations. Formal Methods in System Design\u00a043(1), 93\u2013120 (2013)","journal-title":"Formal Methods in System Design"},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 415\u2013418. Springer, Heidelberg (2006)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"issue":"6","key":"26_CR15","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/1809028.1806630","volume":"45","author":"Sumit Gulwani","year":"2010","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. In: Zorn, B.G., Aiken, A. (eds.) PLDI, pp. 292\u2013304. ACM (2010)","journal-title":"ACM SIGPLAN Notices"},{"issue":"1","key":"26_CR16","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1145\/1328897.1328459","volume":"43","author":"Ashutosh Gupta","year":"2008","unstructured":"Gupta, A., Henzinger, T.A., Majumdar, R., Rybalchenko, A., Xu, R.-G.: Proving non-termination. In: POPL, pp. 147\u2013158 (2008)","journal-title":"ACM SIGPLAN Notices"},{"key":"26_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-642-15769-1_19","volume-title":"Static Analysis","author":"W.R. Harris","year":"2010","unstructured":"Harris, W.R., Lal, A., Nori, A.V., Rajamani, S.K.: Alternation for termination. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 304\u2013319. Springer, Heidelberg (2010)"},{"key":"26_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-88387-6_10","volume-title":"Automated Technology for Verification and Analysis","author":"D. Kroening","year":"2008","unstructured":"Kroening, D., Sharygina, N., Tonetta, S., Tsitovich, A., Wintersteiger, C.M.: Loop summarization using abstract transformers. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 111\u2013125. Springer, Heidelberg (2008)"},{"key":"26_CR19","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":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"26_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"750","DOI":"10.1007\/978-3-540-71493-4_76","volume-title":"Hybrid Systems: Computation and Control","author":"A. Podelski","year":"2007","unstructured":"Podelski, A., Wagner, S.: A sound and complete proof rule for region stability of hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol.\u00a04416, pp. 750\u2013753. Springer, Heidelberg (2007)"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-14295-6_7","volume-title":"Computer Aided Verification","author":"A. Rybalchenko","year":"2010","unstructured":"Rybalchenko, A.: Constraint solving for program verification: Theory and practice by example. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 57\u201371. Springer, Heidelberg (2010)"},{"key":"26_CR24","volume-title":"Theory of linear and integer programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Inc., New York (1986)"},{"key":"26_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification","author":"A. Tiwari","year":"2004","unstructured":"Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 70\u201382. Springer, Heidelberg (2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-02444-8_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T00:22:01Z","timestamp":1558052521000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-02444-8_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319024431","9783319024448"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-02444-8_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}