{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T07:12:41Z","timestamp":1765609961411},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T00:00:00Z","timestamp":1573603200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T00:00:00Z","timestamp":1573603200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2020,12]]},"DOI":"10.1007\/s10009-019-00549-9","type":"journal-article","created":{"date-parts":[[2019,11,13]],"date-time":"2019-11-13T14:02:41Z","timestamp":1573653761000},"page":"655-666","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["On ranking functions for single-path linear-constraint loops"],"prefix":"10.1007","volume":"22","author":[{"given":"Yi","family":"Li","sequence":"first","affiliation":[]},{"given":"Wenyuan","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Yong","family":"Feng","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,13]]},"reference":[{"key":"549_CR1","volume-title":"Infinite Dimensional Analysis: A Hitchhiker\u2019s Guide","author":"C Alipranties","year":"2006","unstructured":"Alipranties, C., Border, K.: Infinite Dimensional Analysis: A Hitchhiker\u2019s Guide. Springer, Berlin (2006)"},{"key":"549_CR2","doi-asserted-by":"crossref","unstructured":"Bagnara, R., Mesnard, F.: Eventual linear ranking functions. In: PPDP\u201915, pp. 229\u2013238. ACM, Madrid (2013)","DOI":"10.1145\/2505879.2505884"},{"key":"549_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":"549_CR4","first-page":"601","volume-title":"CAV\u201917","author":"A Ben-Amram","year":"2017","unstructured":"Ben-Amram, A., Genaim, S.: On multiphase-linear ranking functions. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV\u201917, vol. 10427, pp. 601\u2013620. Springer, Berlin (2017)"},{"issue":"4","key":"549_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2629488","volume":"61","author":"A Ben-Amram","year":"2014","unstructured":"Ben-Amram, A., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 1\u201355 (2014)","journal-title":"J. ACM"},{"issue":"2\u20134","key":"549_CR6","first-page":"699","volume":"16","author":"J Borwein","year":"2009","unstructured":"Borwein, J., Moors, W.: Stability of closedness of convex cones under linear mappings. J. Conv. Anal. 16(2\u20134), 699\u2013705 (2009)","journal-title":"J. Conv. Anal."},{"key":"549_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804441","volume-title":"Convex Optimization","author":"S Boyd","year":"2004","unstructured":"Boyd, S., Vandenberghe, L.: Convex Optimization. Cambridge University Press, New York (2004)"},{"key":"549_CR8","first-page":"491","volume-title":"CAV\u201905","author":"A Bradley","year":"2005","unstructured":"Bradley, A., Manna, Z., Sipma, H.: Linear ranking with reachability. In: Etessami, K., Rajamani, S. (eds.) CAV\u201905, vol. 3576, pp. 491\u2013504. Springer, Berlin (2005)"},{"key":"549_CR9","first-page":"372","volume-title":"CAV\u201906","author":"M Braverman","year":"2006","unstructured":"Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R. (eds.) CAV\u201906, vol. 4144, pp. 372\u2013385. Springer, Berlin (2006)"},{"key":"549_CR10","doi-asserted-by":"crossref","unstructured":"Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking functions by solving semi-algebraic systems. In: ICTAC\u201907, vol. 4711, pp. 34\u201349. Springer (2007)","DOI":"10.1007\/978-3-540-75292-9_3"},{"key":"549_CR11","doi-asserted-by":"crossref","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: TACAS\u201901, vol. 2031, pp. 67\u201381. Springer (2001)","DOI":"10.1007\/3-540-45319-9_6"},{"key":"549_CR12","doi-asserted-by":"crossref","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: TACAS\u201913, vol. 7795, pp. 47\u201361. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"549_CR13","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, In: Lagrangian Relaxation and Semidefinite Programming. VMCAI\u201905, vol. 3385, pp. 1\u201324. Springer (2005)","DOI":"10.1007\/978-3-540-30579-8_1"},{"key":"549_CR14","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511616723","volume-title":"Multidimensional Real Analysis","author":"J Duistermaat","year":"2004","unstructured":"Duistermaat, J., Kolk, J.: Multidimensional Real Analysis. Cambridge University Press, Cambridge (2004)"},{"issue":"5","key":"549_CR15","doi-asserted-by":"publisher","first-page":"313","DOI":"10.1007\/BF01407835","volume":"21","author":"P Feautrier","year":"1992","unstructured":"Feautrier, P.: Some efficient solutions to the affine scheduling problem. I. One-dimensional timed. Int. J. Paral. Prog. 21(5), 313\u2013347 (1992)","journal-title":"Int. J. Paral. Prog."},{"key":"549_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-74759-0","volume-title":"Encyclopedia of Optimization","author":"C Floudas","year":"2009","unstructured":"Floudas, C., Pardalos, P.: Encyclopedia of Optimization. Springer, Berlin (2009)"},{"key":"549_CR17","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Leike, J., Podelski, A.: Linear ranking for linear lasso programs. In: ATVA\u201913, vol. 8172, pp. 365\u2013380. Springer (2013)","DOI":"10.1007\/978-3-319-02444-8_26"},{"key":"549_CR18","doi-asserted-by":"crossref","unstructured":"Jing, R., Moreno Maza, M.: Computing the integer points of a polyhedron, I: algorithm. In: CASC2017, pp. 225\u2013241. Springer (2017)","DOI":"10.1007\/978-3-319-66320-3_17"},{"key":"549_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24488-9","volume-title":"Combinatorial Optimization: Theory and Algorithms","author":"B Korte","year":"2012","unstructured":"Korte, B., Vygen, J.: Combinatorial Optimization: Theory and Algorithms, 5th edn. Springer, Berlin (2012)","edition":"5"},{"issue":"1","key":"549_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-11(1:16)2015","volume":"11","author":"J Leike","year":"2015","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. Log. Methods Comput. Sci. 11(1), 1\u201327 (2015)","journal-title":"Log. Methods Comput. Sci."},{"key":"549_CR21","doi-asserted-by":"crossref","unstructured":"Leike, J., Heizmann, M.: Geometric nontermination arguments. In: TACAS\u201918, vol. 10806, pp. 266\u2013283. Springer (2018)","DOI":"10.1007\/978-3-319-89963-3_16"},{"key":"549_CR22","doi-asserted-by":"crossref","unstructured":"Li, Y., Zhu, G., Feng, Y.: The L-depth eventual linear ranking functions for single-path linear constraints loops. In: TASE\u201916, pp. 30\u201337. IEEE (2016)","DOI":"10.1109\/TASE.2016.8"},{"key":"549_CR23","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.tcs.2017.03.036","volume":"681","author":"Y Li","year":"2017","unstructured":"Li, Y.: Witness to non-termination of linear programs. Theor. Comput. Sci. 681, 75\u2013100 (2017)","journal-title":"Theor. Comput. Sci."},{"key":"549_CR24","first-page":"1284","volume":"27","author":"J Liu","year":"2014","unstructured":"Liu, J., Xu, M., Zhan, N.J., Zhao, H.J.: Discovering non-terminating inputs for multi-path polynomial programs. J. Syst. Sci. Complex. 27, 1284\u20131304 (2014)","journal-title":"J. Syst. Sci. Complex."},{"key":"549_CR25","doi-asserted-by":"crossref","unstructured":"Ouaknine, J., Sousa Pinto, J., Worrell, J.: On termination of integer linear loops. In: SODA\u201915, pp. 957\u201369. SIAM (2015)","DOI":"10.1137\/1.9781611973730.65"},{"key":"549_CR26","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: VMCAI\u201904, vol. 2937, pp. 239\u2013251. Springer (2004)","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"549_CR27","unstructured":"Rebiha,R., Matringe, N., Moura,A.: Generating asymptotically non-terminant initial variable values for linear diagonalizable programs. In: Symbolic Computation in Software Science, SCSS\u201913, pp. 81\u201392 (2013)"},{"key":"549_CR28","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)"},{"key":"549_CR29","first-page":"216","volume-title":"Proceedings of the Symposium on Principles of Database Systems","author":"K Sohn","year":"1991","unstructured":"Sohn, K., Gelder, A.: Termination detection in logic programs using argument sizes. In: Rosenkrantz, D.J. (ed.) Proceedings of the Symposium on Principles of Database Systems, pp. 216\u2013226. ACM, New York (1991)"},{"key":"549_CR30","doi-asserted-by":"crossref","unstructured":"Tiwari, A.: Termination of linear programs. In: CAV\u201904, pp. 70\u201382. Springer (2004)","DOI":"10.1007\/978-3-540-27813-9_6"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00549-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-019-00549-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-019-00549-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,12]],"date-time":"2020-11-12T20:08:46Z","timestamp":1605211726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-019-00549-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,11,13]]},"references-count":30,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2020,12]]}},"alternative-id":["549"],"URL":"https:\/\/doi.org\/10.1007\/s10009-019-00549-9","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,13]]},"assertion":[{"value":"13 November 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}