{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,8]],"date-time":"2025-09-08T06:07:59Z","timestamp":1757311679117},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642397981"},{"type":"electronic","value":"9783642397998"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-39799-8_27","type":"book-chapter","created":{"date-parts":[[2013,7,10]],"date-time":"2013-07-10T23:13:06Z","timestamp":1373497986000},"page":"397-412","source":"Crossref","is-referenced-by-count":16,"title":["Proving Termination Starting from the End"],"prefix":"10.1007","author":[{"given":"Pierre","family":"Ganty","sequence":"first","affiliation":[]},{"given":"Samir","family":"Genaim","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"27_CR1","unstructured":"Acabar, \n                    \n                      http:\/\/loopkiller.com\/acabar"},{"key":"27_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/978-3-540-92188-2_5","volume-title":"Formal Methods for Components and Objects","author":"E. Albert","year":"2008","unstructured":"Albert, E., Arenas, P., Genaim, S., Puebla, G., Zanardini, D.: COSTA: Design and implementation of a cost and termination analyzer for java bytecode. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol.\u00a05382, pp. 113\u2013132. Springer, Heidelberg (2008)"},{"key":"27_CR3","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.\u00a06337, pp. 117\u2013133. Springer, Heidelberg (2010)"},{"key":"27_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-642-02658-4_12","volume-title":"Computer Aided Verification","author":"A.M. Ben-Amram","year":"2009","unstructured":"Ben-Amram, A.M.: Size-change termination, monotonicity constraints and ranking functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 109\u2013123. Springer, Heidelberg (2009)"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"Ben-Amram, A.M., Genaim, S.: On the linear ranking problem for integer linear-constraint loops. In: POPL 2013: Proc. 40th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pp. 51\u201362. ACM (2013)","DOI":"10.1145\/2480359.2429078"},{"key":"27_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"252","DOI":"10.1007\/978-3-642-28756-5_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozga","year":"2012","unstructured":"Bozga, M., Iosif, R., Kone\u010dn\u00fd, F.: Deciding conditional termination. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 252\u2013266. Springer, Heidelberg (2012)"},{"key":"27_CR7","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":"27_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-642-33125-1_28","volume-title":"Static Analysis","author":"H.Y. Chen","year":"2012","unstructured":"Chen, H.Y., Flur, S., Mukhopadhyay, S.: Termination proofs for linear simple loops. In: Min\u00e9, A., Schmidt, D. (eds.) SAS 2012. LNCS, vol.\u00a07460, pp. 422\u2013438. Springer, Heidelberg (2012)"},{"key":"27_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1007\/978-3-540-70545-1_32","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2008","unstructured":"Cook, B., Gulwani, S., Lev-Ami, T., Rybalchenko, A., Sagiv, M.: Proving conditional termination. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 328\u2013340. Springer, Heidelberg (2008)"},{"key":"27_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/11547662_8","volume-title":"Static Analysis","author":"B. Cook","year":"2005","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 87\u2013101. Springer, Heidelberg (2005)"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: PLDI 2006: Proc. 27th ACM-SIGPLAN Conf. on Programming Language Design and Implementation, pp. 415\u2013426. ACM (2006)","DOI":"10.1145\/1133981.1134029"},{"key":"27_CR12","unstructured":"Cousot, P.: M\u00e9thodes It\u00e9ratives de construction et d\u2019approximation de points fixes d\u2019op\u00e9rateurs monotones sur un treillis, analyse s\u00e9mantique de programmes. Th\u00e8se d\u2019\u00e9tat \u00e8s sciences math\u00e9matiques, Universit\u00e9 scientifique et m\u00e9dicale de Grenoble (March 1978) (in French)"},{"key":"27_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44914-0_1","volume-title":"Abstraction, Reformulation, and Approximation","author":"P. Cousot","year":"2000","unstructured":"Cousot, P.: Partial completeness of abstract fixpoint checking, invited paper. In: Choueiry, B.Y., Walsh, T. (eds.) SARA 2000. LNCS (LNAI), vol.\u00a01864, pp. 1\u201325. Springer, Heidelberg (2000)"},{"key":"27_CR14","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: POPL 1977: Proc. 4th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pp. 238\u2013252. ACM (1977)","DOI":"10.1145\/512950.512973"},{"key":"27_CR15","volume-title":"Introduction to Lattices and Order","author":"B.A. Davey","year":"1989","unstructured":"Davey, B.A., Priestley, H.A.: Introduction to Lattices and Order. CUP, Cambridge (1989)"},{"key":"27_CR16","unstructured":"Ganty, P.: The Fixpoint Checking Problem: An Abstraction Refinement Perspective. Ph.D. thesis, Universit\u00e9 Libre de Bruxelles (2007)"},{"key":"27_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-63166-6_10","volume-title":"Computer Aided Verification","author":"S. Graf","year":"1997","unstructured":"Graf, S., Sa\u00efdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 72\u201383. Springer, Heidelberg (1997)"},{"key":"27_CR18","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.M.: Termination analysis with compositional transition invariants. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 89\u2013103. Springer, Heidelberg (2010)"},{"key":"27_CR19","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: Proc. 28th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pp. 81\u201392. ACM (2001)","DOI":"10.1145\/373243.360210"},{"key":"27_CR20","unstructured":"Park, D.: Fixpoint induction and proofs of program properties. In: Machine Intelligence, vol.\u00a05, pp. 59\u201378. American Elsevier (1969)"},{"key":"27_CR21","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":"27_CR22","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004: Proc. 19th Annual IEEE Symp. on Logic in Computer Science, pp. 32\u201341. IEEE (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"27_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-540-70545-1_31","volume-title":"Computer Aided Verification","author":"A. Podelski","year":"2008","unstructured":"Podelski, A., Rybalchenko, A., Wies, T.: Heap assumptions on demand. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 314\u2013327. Springer, Heidelberg (2008)"},{"key":"27_CR24","first-page":"264","volume":"30","author":"F.P. Ramsey","year":"1929","unstructured":"Ramsey, F.P.: On a problem of formal logic. London Math. Society\u00a030, 264\u2013286 (1929)","journal-title":"London Math. Society"},{"key":"27_CR25","unstructured":"Rybalchenko, A.: Armc (2008), \n                    \n                      http:\/\/www7.in.tum.de\/~rybal\/armc\/"},{"key":"27_CR26","unstructured":"Rybalchenko, A.: Personal communication (2012)"},{"key":"27_CR27","doi-asserted-by":"crossref","unstructured":"Spoto, F., Mesnard, F., Payet, \u00c9.: A termination analyzer for java bytecode based on path-length. ACM Trans. Program. Lang. Syst. 32(3) (2010)","DOI":"10.1145\/1709093.1709095"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-39799-8_27","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T18:39:46Z","timestamp":1557945586000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-39799-8_27"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642397981","9783642397998"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-39799-8_27","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}