{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:47:51Z","timestamp":1757314071171,"version":"3.40.3"},"publisher-location":"Cham","reference-count":29,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319216676"},{"type":"electronic","value":"9783319216683"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-21668-3_18","type":"book-chapter","created":{"date-parts":[[2015,7,13]],"date-time":"2015-07-13T11:08:53Z","timestamp":1436785733000},"page":"304-321","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions"],"prefix":"10.1007","author":[{"given":"Amir M.","family":"Ben-Amram","sequence":"first","affiliation":[]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,7,14]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"18_CR2","doi-asserted-by":"crossref","first-page":"304","DOI":"10.1007\/978-3-319-21668-3_18","volume-title":"Computer Aided Verification","author":"Amir M. Ben-Amram","year":"2015","unstructured":"Ben-Amram, A., Genaim, S.: Complexity of Bradley-Manna-Sipma lexicographic ranking functions. In: CoRR, abs\/1504.05018 (2015)"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M.: Monotonicity constraints for termination in the integer domain. Logical Methods in Comput. Sci. 7(3) (2011)","DOI":"10.2168\/LMCS-7(3:4)2011"},{"issue":"4","key":"18_CR4","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/2629488","volume":"61","author":"AM Ben-Amram","year":"2014","unstructured":"Ben-Amram, A.M., Genaim, S.: Ranking functions for linear-constraint loops. J. ACM 61(4), 26:1\u201326:55 (2014)","journal-title":"J. ACM"},{"key":"18_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":"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":"18_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":"AR 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. 3580, pp. 1349\u20131361. Springer, Heidelberg (2005)"},{"key":"18_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":"AR 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. 3653, pp. 488\u2013502. Springer, Heidelberg (2005)"},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-30579-8_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"18_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"18_CR10","series-title":"LNCS","first-page":"67","volume-title":"TACAS 2001","author":"M Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"18_CR11","series-title":"LNCS","first-page":"442","volume-title":"CAV 2002","author":"M Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, D., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"issue":"1","key":"18_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 43(1), 93\u2013120 (2013)","journal-title":"Formal Methods in System Design"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/978-3-642-36742-7_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"B Cook","year":"2013","unstructured":"Cook, B., See, A., Zuleger, F.: Ramsey vs. lexicographic termination proving. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 47\u201361. Springer, Heidelberg (2013)"},{"issue":"5","key":"18_CR14","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 time. Int. J. Parallel Prog. 21(5), 313\u2013347 (1992)","journal-title":"Int. J. Parallel Prog."},{"issue":"6","key":"18_CR15","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/BF01379404","volume":"21","author":"P Feautrier","year":"1992","unstructured":"Feautrier, P.: Some efficient solutions to the affine scheduling problem. II. Multidimensional time. Int. J. Parallel Prog. 21(6), 389\u2013420 (1992)","journal-title":"Int. J. Parallel Prog."},{"key":"18_CR16","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"XIX","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. XIX, 19\u201332 (1967)","journal-title":"Proc. Symp. Appl. Math."},{"key":"18_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":"WR 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. 6337, pp. 304\u2013319. Springer, Heidelberg (2010)"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-54862-8_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Leike","year":"2014","unstructured":"Leike, J., Heizmann, M.: Ranking templates for linear loops. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 172\u2013186. Springer, Heidelberg (2014)"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Larraz, D., Oliveras, A., Rodr\u00edguez-Carbonell, E., Rubio, A.: Proving termination of imperative programs using Max-SMT. In: Formal Methods in Computer-Aided Design, FMCAD 2013, pp. 218\u2013225. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679413"},{"key":"18_CR20","unstructured":"L\u00e1szl\u00f3, L.: Coverings and colorings of hypergraphs. In: Proceedings of the 4th Southeastern Conference on Combinatorics, Graph Theory, and Computing, pp. 3\u201312 (1973)"},{"issue":"1","key":"18_CR21","first-page":"111","volume":"8","author":"F Mesnard","year":"2008","unstructured":"Mesnard, F., Serebrenik, A.: Recurrence with affine level mappings is P-time decidable for CLP(R). TPLP 8(1), 111\u2013119 (2008)","journal-title":"TPLP"},{"issue":"1","key":"18_CR22","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/BF02579160","volume":"4","author":"KT Phelps","year":"1984","unstructured":"Phelps, K.T., R\u00f6dl, V.: On the algorithmic complexity of coloring simple hypergraphs and steiner triple systems. Combinatorica 4(1), 79\u201388 (1984)","journal-title":"Combinatorica"},{"key":"18_CR23","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. 2937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"18_CR24","unstructured":"Rybalchenko, A.: Temporal verification with transition invariants. Ph.D. thesis, Universit\u00e4t des Saarlandes (2004)"},{"key":"18_CR25","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1986)"},{"key":"18_CR26","first-page":"216","volume-title":"Symposium on Principles of Database Systems","author":"K Sohn","year":"1991","unstructured":"Sohn, K., Van Gelder, A.: Termination detection in logic programs using argument sizes. In: Rosenkrantz, D.J. (ed.) Symposium on Principles of Database Systems, pp. 216\u2013226. ACM Press, New York (1991)"},{"issue":"1","key":"18_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0304-3975(76)90061-X","volume":"3","author":"LJ Stockmeyer","year":"1976","unstructured":"Stockmeyer, L.J.: The polynomial-time hierarchy. Theor. Comput. Sci. 3(1), 1\u201322 (1976)","journal-title":"Theor. Comput. Sci."},{"key":"18_CR28","unstructured":"Turing, A.M.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67\u201369, 1948. reprinted. In: The early British computer conferences, Charles Babbage Institute Reprint Series For The History Of Computing, vol. 14. MIT Press (1989)"},{"key":"18_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-642-54833-8_22","volume-title":"Programming Languages and Systems","author":"C Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: An abstract domain to infer ordinal-valued ranking functions. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 412\u2013431. Springer, Heidelberg (2014)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-21668-3_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,22]],"date-time":"2019-07-22T20:14:57Z","timestamp":1563826497000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-21668-3_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319216676","9783319216683"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-21668-3_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]},"assertion":[{"value":"14 July 2015","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}