{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:28:36Z","timestamp":1770283716085,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540787389","type":"print"},{"value":"9783540787396","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-78739-6_13","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T08:39:06Z","timestamp":1207125546000},"page":"148-162","source":"Crossref","is-referenced-by-count":17,"title":["Ranking Abstractions"],"prefix":"10.1007","author":[{"given":"Aziem","family":"Chawdhary","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sumit","family":"Gulwani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/11562436_1","volume-title":"Formal Techniques for Networked and Distributed Systems - FORTE 2005","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Pnueli, A., Zuck, L.: Ranking abstraction as companion to predicate abstraction. In: Wang, F. (ed.) FORTE 2005. LNCS, vol.\u00a03731, Springer, Heidelberg (2005)"},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.: Variance analyses from invariance analyses. In: POPL 2007 (2007)","DOI":"10.1145\/1190216.1190249"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Bradley","year":"2005","unstructured":"Bradley, A., Manna, Z., Sipma, H.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, Springer, Heidelberg (2005)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Bruynooghe, M., Codish, M., Gallagher, J., Genaim, S., Vanhoof, W.: Termination analysis through combination of type based norms. ACM Trans. Progam. Lang. Syst.\u00a029(2) (2007)","DOI":"10.1145\/1216374.1216378"},{"key":"13_CR5","unstructured":"Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., Yang, H.: Ranking abstractions. Manuscript (2008), http:\/\/www.dcs.qmul.ac.uk\/~aiem\/paper\/esop08-full.pdf"},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. The Journal of Logic Programming\u00a041(1) (1999)","DOI":"10.1016\/S0743-1066(99)00006-0"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006 (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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, Springer, Heidelberg (2006)"},{"issue":"1\u20132","key":"13_CR9","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/S0304-3975(00)00313-3","volume":"277","author":"P. Cousot","year":"2002","unstructured":"Cousot, P.: Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Theoretical Comput. Sci.\u00a0277(1\u20132), 47\u2013103 (2002)","journal-title":"Theoretical Comput. Sci."},{"key":"13_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979 (1979)","DOI":"10.1145\/567752.567778"},{"key":"13_CR11","unstructured":"Detlefs, D., Nelson, G., Saxe, J.: Simplify: A theorem prover for program checking (2003)"},{"key":"13_CR12","unstructured":"Jeannet, B.: NewPolka polyhedra library, http:\/\/pop-art.inrialpes.fr\/people\/bjeannet\/newpolka\/index.html"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL 2001 (2001)","DOI":"10.1145\/360204.360210"},{"key":"13_CR14","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s10990-006-8609-1","volume":"19","author":"A. Min\u00e9","year":"2006","unstructured":"Min\u00e9, A.: The Octagon abstract domain. Higher-Order and Symbolic Comput.\u00a019, 31\u2013100 (2006)","journal-title":"Higher-Order and Symbolic Comput."},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G. Necula","year":"2002","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, Springer, Heidelberg (2002)"},{"key":"13_CR16","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2004)"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"13_CR18","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.\u00a014, MIT Press, Cambridge (1989)"},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Yahav, E., Reps, T., Sagiv, M., Wilhelm, R.: Verifying temporal heap properties specified via evolution logic. Logic Journal of IGPL (September 2006)","DOI":"10.1093\/jigpal\/jzl009"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78739-6_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T11:20:45Z","timestamp":1619522445000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78739-6_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540787389","9783540787396"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78739-6_13","relation":{},"subject":[]}}