{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,11,19]],"date-time":"2024-11-19T16:38:06Z","timestamp":1732034286664},"publisher-location":"Berlin, Heidelberg","reference-count":35,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642331244"},{"type":"electronic","value":"9783642331251"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33125-1_28","type":"book-chapter","created":{"date-parts":[[2012,8,29]],"date-time":"2012-08-29T02:47:24Z","timestamp":1346208444000},"page":"422-438","source":"Crossref","is-referenced-by-count":13,"title":["Termination Proofs for Linear Simple Loops"],"prefix":"10.1007","author":[{"given":"Hong Yi","family":"Chen","sequence":"first","affiliation":[]},{"given":"Shaked","family":"Flur","sequence":"additional","affiliation":[]},{"given":"Supratik","family":"Mukhopadhyay","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/11609773_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"I. Balaban","year":"2005","unstructured":"Balaban, I., Cohen, A., Pnueli, A.: Ranking Abstraction of Recursive Programs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 267\u2013281. Springer, Heidelberg (2005)"},{"key":"28_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-642-27940-9_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.M. Ben-Amram","year":"2012","unstructured":"Ben-Amram, A.M., Genaim, S., Masud, A.N.: On the Termination of Integer Loops. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol.\u00a07148, pp. 72\u201387. Springer, Heidelberg (2012)"},{"key":"28_CR3","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1145\/1190216.1190249","volume-title":"Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007","author":"J. Berdine","year":"2007","unstructured":"Berdine, J., Chawdhary, A., Cook, B., Distefano, D., O\u2019Hearn, P.: Variance analyses from invariance analyses. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, pp. 211\u2013224. ACM, New York (2007)"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"386","DOI":"10.1007\/11817963_35","volume-title":"Computer Aided Verification","author":"J. Berdine","year":"2006","unstructured":"Berdine, J., Cook, B., Distefano, D., O\u2019Hearn, P.W.: Automatic Termination Proofs for Programs with Shape-Shifting Heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 386\u2013400. Springer, Heidelberg (2006)"},{"key":"28_CR5","unstructured":"Bradley, A.R.: polyrank: Tools for termination analysis (2005), \n                    \n                      http:\/\/theory.stanford.edu\/~arbrad\/software\/polyrank.html"},{"key":"28_CR6","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":"A.R. 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.\u00a03576, pp. 491\u2013504. Springer, Heidelberg (2005)"},{"key":"28_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":"28_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":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of Polynomial Programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/11817963_34","volume-title":"Computer Aided Verification","author":"M. Braverman","year":"2006","unstructured":"Braverman, M.: Termination of Integer Linear Programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 372\u2013385. Springer, Heidelberg (2006)"},{"key":"28_CR10","unstructured":"Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., Yang, H.: Ranking abstractions. Technical report (2008)"},{"key":"28_CR11","unstructured":"Chen, H.Y., Flur, S., Mukhopadhyay, S.: Lsl test suite, \n                    \n                      https:\/\/tigerbytes2.lsu.edu\/users\/hchen11\/lsl\/"},{"key":"28_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/BFb0028753","volume-title":"Computer Aided Verification","author":"M.A. Colon","year":"1998","unstructured":"Colon, M.A., Uribe, T.E.: Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol.\u00a01427, pp. 293\u2013304. Springer, Heidelberg (1998)"},{"key":"28_CR13","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":"M.A. 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.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"28_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"442","DOI":"10.1007\/3-540-45657-0_36","volume-title":"Computer Aided Verification","author":"M.A. Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M.A., Sipma, H.B.: Practical Methods for Proving Program Termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 442\u2013454. Springer, Heidelberg (2002)"},{"key":"28_CR15","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":"28_CR16","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":"28_CR17","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1145\/1133981.1134029","volume-title":"Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2006","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Proceedings of the 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2006, pp. 415\u2013426. ACM, New York (2006)"},{"key":"28_CR18","doi-asserted-by":"crossref","unstructured":"Cook, B., Rybalchenko, A.: Proving that programs eventually do something good. In: POPL 2006: Principles of Programming Languages, pp. 265\u2013276. Springer (2007)","DOI":"10.1145\/1190215.1190257"},{"key":"28_CR19","first-page":"303","volume-title":"Program Flow Analysis: Theory and Applications","author":"P. Cousot","year":"1981","unstructured":"Cousot, P.: Semantic foundations of program analysis. In: Muchnick, S.S., Jones, N.D. (eds.) Program Flow Analysis: Theory and Applications, ch.\u00a010, pp. 303\u2013342. Prentice-Hall, Inc., Englewood Cliffs (1981)"},{"key":"28_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-30579-8_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"28_CR21","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":"28_CR22","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1145\/1543135.1542518","volume":"44","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Jain, S., Koskinen, E.: Control-flow refinement and progress invariants for bound analysis. SIGPLAN Not.\u00a044, 375\u2013385 (2009)","journal-title":"SIGPLAN Not."},{"key":"28_CR23","first-page":"127","volume-title":"Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009","author":"S. Gulwani","year":"2009","unstructured":"Gulwani, S., Mehra, K.K., Chilimbi, T.: Speed: precise and efficient static estimation of program computational complexity. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 127\u2013139. ACM, New York (2009)"},{"key":"28_CR24","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1145\/1806596.1806630","volume-title":"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010","author":"S. Gulwani","year":"2010","unstructured":"Gulwani, S., Zuleger, F.: The reachability-bound problem. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, pp. 292\u2013304. ACM, New York (2010)"},{"key":"28_CR25","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":"28_CR26","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Software model checking of liveness properties via transition invariants. Technical report (2003)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"28_CR27","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":"28_CR28","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"28_CR29","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition predicate abstraction and fair termination. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005. ACM (2005)","DOI":"10.1145\/1040305.1040317"},{"key":"28_CR30","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1112\/plms\/s2-30.1.264","volume":"30","author":"F.P. Ramsey","year":"1930","unstructured":"Ramsey, F.P.: On a problem of formal logic. Proc. London Math. Soc.\u00a030, 491\u2013504 (1930)","journal-title":"Proc. London Math. Soc."},{"key":"28_CR31","doi-asserted-by":"crossref","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst.\u00a029(5) (August 2007)","DOI":"10.1145\/1275497.1275501"},{"key":"28_CR32","unstructured":"Rybalchenko, A.: Rankfinder, \n                    \n                      http:\/\/www.mpi-sws.org\/~rybal\/rankfinder\/"},{"key":"28_CR33","volume-title":"Theory of linear and integer programming","author":"A. Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of linear and integer programming. John Wiley & Sons, Inc., New York (1986)"},{"key":"28_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification","author":"A. Tiwari","year":"2004","unstructured":"Tiwari, A.: Termination of Linear Programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 70\u201382. Springer, Heidelberg (2004)"},{"key":"28_CR35","unstructured":"Turing, A.M.: Checking a large routine. Report of a Conference on High Speed Automatic Calculating Machines, pp. 67\u201369 (1948)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33125-1_28.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:56:16Z","timestamp":1620114976000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33125-1_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642331244","9783642331251"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33125-1_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}