{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T00:49:15Z","timestamp":1775868555786,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662496732","type":"print"},{"value":"9783662496749","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-662-49674-9_4","type":"book-chapter","created":{"date-parts":[[2016,4,8]],"date-time":"2016-04-08T18:49:00Z","timestamp":1460141340000},"page":"54-70","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["Synthesizing Ranking Functions from Bits and Pieces"],"prefix":"10.1007","author":[{"given":"Caterina","family":"Urban","sequence":"first","affiliation":[]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[]},{"given":"Temesghen","family":"Kahsai","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,4,9]]},"reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M.: Ranking functions for linear-constraint loops. In: VPT, pp. 1\u20138 (2013)","DOI":"10.1145\/2629488"},{"key":"4_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-31424-7_4","volume-title":"Computer Aided Verification","author":"AR Bradley","year":"2012","unstructured":"Bradley, A.R.: IC3 and beyond: incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, p. 4. Springer, Heidelberg (2012)"},{"key":"4_CR3","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":"4_CR4","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":"4_CR5","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":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1007\/978-3-642-54862-8_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H-Y Chen","year":"2014","unstructured":"Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O\u2019Hearn, P.W.: Proving nontermination via safety. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 156\u2013171. Springer, Heidelberg (2014)"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Chen, H.Y., David, C., Kroening, D., Schrammel, P., Wachter, B.: Synthesising interprocedural bit-precise termination proofs. In: ASE (2015)","DOI":"10.1109\/ASE.2015.10"},{"key":"4_CR8","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":"MA 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. 2031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-3-319-21690-4_2","volume-title":"Computer Aided Verification","author":"B Cook","year":"2015","unstructured":"Cook, B., Khlaaf, H., Piterman, N.: On automation of CTL* verification for infinite-state systems. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 13\u201329. Springer, Heidelberg (2015)"},{"issue":"6","key":"4_CR10","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1145\/1133255.1134029","volume":"41","author":"Byron Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI, pp. 415\u2013426 (2006)","journal-title":"ACM SIGPLAN Notices"},{"key":"4_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: POPL, pp. 245\u2013258 (2012)","DOI":"10.1145\/2103621.2103687"},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"4_CR13","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/978-3-319-21668-3_16","volume-title":"Computer Aided Verification","author":"Vijay D\u2019Silva","year":"2015","unstructured":"D\u2019Silva, V., Urban, C.: Conflict-driven conditional termination. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part II. LNCS, vol. 9207, pp. 271\u2013286. Springer, Heidelberg (2015)"},{"key":"4_CR14","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume":"19","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. Proc. Symp. Appl. Math. 19, 19\u201332 (1967)","journal-title":"Proc. Symp. Appl. Math."},{"key":"4_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-3-319-21690-4_20","volume-title":"Computer Aided Verification","author":"A Gurfinkel","year":"2015","unstructured":"Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part I. LNCS, vol. 9206, pp. 343\u2013361. Springer, Heidelberg (2015)"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"455","DOI":"10.1007\/978-3-662-46681-0_43","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Heizmann","year":"2015","unstructured":"Heizmann, M., Dietsch, D., Leike, J., Musa, B., Podelski, A.: Ultimate automizer with array interpolation (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 455\u2013457. Springer, Heidelberg (2015)"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/978-3-642-39799-8_2","volume-title":"Computer Aided Verification","author":"M Heizmann","year":"2013","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36\u201352. Springer, Heidelberg (2013)"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-662-48899-7_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T Kahsai","year":"2015","unstructured":"Kahsai, T., Navas, J.A., Jovanovic, D., Sch\u00e4f, M.: Finding inconsistencies in programs with loops. In: Davis, M., et al. (eds.) LPAR-20 2015. LNCS, vol. 9450, pp. 499\u2013514. Springer, Heidelberg (2015). doi: 10.1007\/978-3-662-48899-7_35"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-08867-9_2","volume-title":"Computer Aided Verification","author":"A Komuravelli","year":"2014","unstructured":"Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 17\u201334. Springer, Heidelberg (2014)"},{"issue":"2","key":"4_CR20","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L.: Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3(2), 125\u2013143 (1977)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO, pp. 75\u201388 (2004)","DOI":"10.1109\/CGO.2004.1281665"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Le, T.-C., Qin, S., Chin, W.-N.: Termination and non-termination specification inference. In: PLDI, pp. 489\u2013498 (2015)","DOI":"10.1145\/2813885.2737993"},{"key":"4_CR23","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\/373243.360210"},{"key":"4_CR24","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. LNCS, vol. 8413, pp. 172\u2013186. Springer, Heidelberg (2014)"},{"issue":"1","key":"4_CR25","first-page":"297","volume":"42","author":"S Ovchinnikov","year":"2002","unstructured":"Ovchinnikov, S.: Max-min representation of piecewise linear functions. Contrib. Algebra Geom. 42(1), 297\u2013302 (2002)","journal-title":"Contrib. Algebra Geom."},{"key":"4_CR26","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":"4_CR27","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"4_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"417","DOI":"10.1007\/978-3-662-46681-0_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Str\u00f6der","year":"2015","unstructured":"Str\u00f6der, T., Aschermann, C., Frohn, F., Hensel, J., Giesl, J.: AProVE: termination and memory safety of C programs (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 417\u2013419. Springer, Heidelberg (2015)"},{"key":"4_CR29","unstructured":"Turing, A.: Checking a large routine. In: Report of a Conference on High Speed Automatic Calculating Machines, pp. 67\u201369 (1948)"},{"key":"4_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"464","DOI":"10.1007\/978-3-662-46681-0_46","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Urban","year":"2015","unstructured":"Urban, C.: FuncTion: an abstract domain functor for termination (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 464\u2013466. Springer, Heidelberg (2015)"},{"key":"4_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/978-3-319-10936-7_19","volume-title":"Static Analysis","author":"C Urban","year":"2014","unstructured":"Urban, C., Min\u00e9, A.: A decision tree abstract domain for proving conditional termination. In: M\u00fcller-Olm, M., Seidl, H. (eds.) SAS 2014. LNCS, vol. 8723, pp. 302\u2013318. Springer, Heidelberg (2014)"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/978-3-662-46081-8_11","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"C Urban","year":"2015","unstructured":"Urban, C., Min\u00e9, A.: Proving guarantee and recurrence temporal properties by abstract interpretation. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 190\u2013208. Springer, Heidelberg (2015)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49674-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T08:26:41Z","timestamp":1748852801000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49674-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783662496732","9783662496749"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49674-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"9 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}