{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T21:00:06Z","timestamp":1725570006511},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642171635"},{"type":"electronic","value":"9783642171642"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-17164-2_12","type":"book-chapter","created":{"date-parts":[[2010,11,19]],"date-time":"2010-11-19T05:54:39Z","timestamp":1290146079000},"page":"156-171","source":"Crossref","is-referenced-by-count":0,"title":["Metric Spaces and Termination Analyses"],"prefix":"10.1007","author":[{"given":"Aziem","family":"Chawdhary","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","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, pp. 1\u201312. Springer, Heidelberg (2005)"},{"key":"12_CR2","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":"A. Bradley","year":"2005","unstructured":"Bradley, A., Manna, Z., Sipma, H.: Termination of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"12_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":"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":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-3-540-78739-6_13","volume-title":"Programming Languages and Systems","author":"A. Chawdhary","year":"2008","unstructured":"Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., Yang, H.: Ranking abstractions. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol.\u00a04960, pp. 148\u2013162. Springer, Heidelberg (2008)"},{"issue":"1","key":"12_CR5","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S0743-1066(99)00006-0","volume":"41","author":"M. Codish","year":"1999","unstructured":"Codish, M., Taboch, C.: A semantic basis for the termination analysis of logic programs. JLP\u00a041(1), 103\u2013123 (1999)","journal-title":"JLP"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Cook, B., Gotsman, A., Podelski, A., Rybalchenko, A., Vardi, M.Y.: Proving that programs eventually do something good. In: POPL 2007 (2007)","DOI":"10.1145\/1190216.1190257"},{"key":"12_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"},{"issue":"3","key":"12_CR8","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/s10703-009-0087-8","volume":"35","author":"B. Cook","year":"2009","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Summarization for termination: no return! Formal Methods in System Design\u00a035(3), 369\u2013387 (2009)","journal-title":"Formal Methods in System Design"},{"issue":"1-2","key":"12_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. Theor. Comput. Sci.\u00a0277(1-2), 47\u2013103 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, pp. 238\u2013252 (January 1977)","DOI":"10.1145\/512950.512973"},{"issue":"4","key":"12_CR11","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1093\/logcom\/2.4.511","volume":"2","author":"P. Cousot","year":"1992","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation frameworks. Journal of Logic and Computation\u00a02(4), 511\u2013547 (1992)","journal-title":"Journal of Logic and Computation"},{"issue":"2","key":"12_CR12","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1016\/j.ic.2008.03.025","volume":"207","author":"P. Cousot","year":"2009","unstructured":"Cousot, P., Cousot, R.: Bi-inductive structural semantics. Information and Computation\u00a0207(2), 258\u2013283 (2009)","journal-title":"Information and Computation"},{"key":"12_CR13","volume-title":"Control flow semantics","author":"J. Bakker de","year":"1996","unstructured":"de Bakker, J., de Vink, E.: Control flow semantics. MIT Press, Cambridge (1996)"},{"key":"12_CR14","unstructured":"Escard\u00f3, M.: A metric model of PCF. unpublished research note (1998)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-27815-3_22","volume-title":"Algebraic Methodology and Software Technology","author":"B. Jeannet","year":"2004","unstructured":"Jeannet, B., Serwe, W.: Abstracting call-stacks for interprocedural verification of imperative programs. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol.\u00a03116, pp. 258\u2013273. Springer, Heidelberg (2004)"},{"key":"12_CR16","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.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. LNCS, vol.\u00a06174, pp. 89\u2013103. Springer, Heidelberg (to appear, 2010)"},{"issue":"3","key":"12_CR17","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1145\/373243.360210","volume":"36","author":"C.S. Lee","year":"2001","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. SIGPLAN Not.\u00a036(3), 81\u201392 (2001)","journal-title":"SIGPLAN Not."},{"key":"12_CR18","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":"12_CR19","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"issue":"1-2","key":"12_CR20","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(00)00403-5","volume":"258","author":"F. Breugel van","year":"2001","unstructured":"van Breugel, F.: An introduction to metric semantics: operational and denotational models for programming and specification languages. Theoretical Computer Science\u00a0258(1-2), 1\u201398 (2001)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-17164-2_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,22]],"date-time":"2019-03-22T05:48:51Z","timestamp":1553233731000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-17164-2_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642171635","9783642171642"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-17164-2_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}