{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,2]],"date-time":"2023-01-02T00:50:30Z","timestamp":1672620630833},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2013,8,14]],"date-time":"2013-08-14T00:00:00Z","timestamp":1376438400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,2]]},"DOI":"10.1007\/s10009-013-0288-8","type":"journal-article","created":{"date-parts":[[2013,8,13]],"date-time":"2013-08-13T17:12:32Z","timestamp":1376413952000},"page":"47-57","source":"Crossref","is-referenced-by-count":6,"title":["Termination proofs for linear simple loops"],"prefix":"10.1007","volume":"17","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","published-online":{"date-parts":[[2013,8,14]]},"reference":[{"key":"288_CR1","doi-asserted-by":"crossref","unstructured":"Balaban, I., Cohen, A., Pnueli, A.: Ranking abstraction of recursive programs. In: Proceedings of the verification, model checking, and abstract interpretation (VMCAI06), pp. 267\u2013281. Springer, Berlin (2006)","DOI":"10.1007\/11609773_18"},{"key":"288_CR2","doi-asserted-by":"crossref","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 \u201907), New York, NY, USA, pp. 211\u2013224 (2007) (ISBN 1-59593-575-4)","DOI":"10.1145\/1190216.1190249"},{"key":"288_CR3","doi-asserted-by":"crossref","unstructured":"Berdine, J., Cook, B., Distefano, D., OHearn, P. W.: Automatic termination proofs for programs with shape-shifting heaps. In: Proceedings of the 18th international conference on computer aided verification (CAV), lecture notes in computer science vol. 4144, pp. 386\u2013400 (2006)","DOI":"10.1007\/11817963_35"},{"key":"288_CR4","unstructured":"Bradley, A.R.: polyrank: tools for termination analysis. http:\/\/theory.stanford.edu\/arbrad\/software\/polyrank.html (2005)"},{"key":"288_CR5","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Linear ranking with reachability. In: Proceedings of the computer aided verification (CAV), pp. 491\u2013504. Springer, Berlin (2005)","DOI":"10.1007\/11513988_48"},{"key":"288_CR6","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination of polynomial programs. In: Proceedings of the verification, model checking, and abstract interpretation (VMCAI2005), vol. 3385 of LNCS, pp. 113\u2013129. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-30579-8_8"},{"key":"288_CR7","doi-asserted-by":"crossref","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: The polyranking principle. In: Proceedings of the 32nd international colloquim on automata, languages and programming (ICALP), Lisbon, Portugal, 11\u201315 July 2005, pp. 1349\u20131361. Springer, Berlin (2005)","DOI":"10.1007\/11523468_109"},{"key":"288_CR8","doi-asserted-by":"crossref","unstructured":"Braverman, M.: Termination of integer linear programs. In: Proceedings of the 18th international conference on computer aided verification (CAV), lecture notes in computer science vol. 4144, pp. 372\u2013385 (2006)","DOI":"10.1007\/11817963_34"},{"key":"288_CR9","unstructured":"Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., Hongseok Y.:Ranking abstractions, Technical report (2008)"},{"key":"288_CR10","unstructured":"Yi Chen, H., Flur, S., Mukhopadhyay, S.: LSL test suite. https:\/\/tigerbytes2.lsu.edu\/users\/hchen11\/lsl\/"},{"key":"288_CR11","doi-asserted-by":"crossref","unstructured":"Colon, M. , Uribe, T.: Generating finite-state abstractions of reactive systems using decision procedures. In:Proceedings of the computer aided verification (CAV), pp. 293\u2013304. Springer, Berlin (1998)","DOI":"10.1007\/BFb0028753"},{"key":"288_CR12","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: Proceedings of the 7th international conference on tools and algorithms for the construction and analysis of systems (TACAS 2001), pp. 67\u201381. Springer, London (2001) (ISBN 3-540-41865-2) http:\/\/dl.acm.org\/citation.cfm?id=646485.694449"},{"key":"288_CR13","unstructured":"Col\u00f3n, M., Sipma, H.: Practical methods for proving program termination. In: Proceedings of the 14th international conference on computer aided verification (CAV \u201902), pp. 442\u2013454. Springer, London (2002) (ISBN 3-540-43997-8). http:\/\/dl.acm.org\/citation.cfm?id=647771.734281"},{"key":"288_CR14","doi-asserted-by":"crossref","unstructured":"Cook, B., Gulwani S., Lev-ami, T., Rybalchenko, A., S.: Mooly proving conditional termination. In: Proceedings of the computer aided verification (CAV) lecture notes in computer science vol. 5123, pp. 328\u2013340. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-70545-1_32"},{"key":"288_CR15","doi-asserted-by":"crossref","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Abstraction refinement for termination. In: Proceedings of the static analysis symposium (SAS2005), vol. 3672 of LNCS, pp. 87\u2013101. Springer, Berlin (2005)","DOI":"10.1007\/11547662_8"},{"key":"288_CR16","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 \u201906), pp. 415\u2013426. New York, NY, USA, (2006) (ISBN 1-59593-320-4)"},{"key":"288_CR17","doi-asserted-by":"crossref","unstructured":"Cook, B., Rybalchenko, A.: Proving that programs eventually do something good. In: Proceedings of the principles of programming languages (POPL06), pp. 265\u2013276. Springer, Berlin (2007)","DOI":"10.1145\/1190216.1190257"},{"key":"288_CR18","doi-asserted-by":"crossref","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Proceedings of the 6th international conference on verification, model checking and abstract interpretation (VMCAI\u201905), pp. 1\u201324. Paris, LNCS 3385, Springer, Berlin (2005) (ISBN 978-3-540-24297-0). doi: 10.1007\/b105073 , http:\/\/www.springerlink.com\/content\/qkufe4uekjgyja4f","DOI":"10.1007\/b105073"},{"key":"288_CR19","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: An abstract interpretation framework for termination. In: Field, J., Hicks, M. (eds.) Proceedings of the 39th ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), Philadelphia, USA, 22\u201328 Jan 2012, pp. 245\u2013258. ACM (2012) (ISBN 978-1-4503-1083-3)","DOI":"10.1145\/2103621.2103687"},{"key":"288_CR20","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Jain, S., Koskinen E.: Control-flow refinement and progress invariants for bound analysis. SIGPLAN Not. 44, 375\u2013385, (2009) (ISSN 0362\u20131340)","DOI":"10.1145\/1543135.1542518"},{"key":"288_CR21","doi-asserted-by":"crossref","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 \u201909), pp. 127\u2013139. New York, NY, USA, ACM (2009) (ISBN 978-1-60558-379-2)","DOI":"10.1145\/1480881.1480898"},{"key":"288_CR22","doi-asserted-by":"crossref","unstructured":"Kroening, D., Sharygina, N., Tsitovich, A., Wintersteiger, C., Termination analysis with compositional transition invariants. In: Proceedings of CAV, vol. 6174 of LNCS, pp. 89\u2013103. Springer, Berlin (2010) (ISBN 978-3-642-14294-9)","DOI":"10.1007\/978-3-642-14295-6_9"},{"key":"288_CR23","unstructured":"Podelski, A., Rybalchenk, A.: Software model checking of liveness properties via transition invariants. Technical report (2003)"},{"key":"288_CR24","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Proceedings of the VMCAI, pp. 239\u2013251 (2004)","DOI":"10.1007\/978-3-540-24622-0_20"},{"key":"288_CR25","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: Proceedings of the LICS, pp. 32\u201341 (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"288_CR26","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 \u201905). ACM (2005)","DOI":"10.1145\/1040305.1040317"},{"key":"288_CR27","doi-asserted-by":"crossref","unstructured":"Ramsey, F.P.: On a problem of formal logic. In: Proceedings of the London Mathematical Society, vol. 30, pp. 491\u2013504 (1930)","DOI":"10.1112\/plms\/s2-30.1.264"},{"key":"288_CR28","unstructured":"RankFinder, A.R.: http:\/\/www.mpi-sws.org\/ybal\/rankfinder\/"},{"key":"288_CR29","unstructured":"Schrijver, A.: Theory of linear and integer programming. Wiley, New York (1986) (ISBN 0-471-90854-1)"},{"key":"288_CR30","doi-asserted-by":"crossref","unstructured":"Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D. (eds.) Proceedings of the CAV, vol. 3114 of lecture notes in computer science, pp. 70\u201382. Springer, Berlin (2004) (ISBN 3-540-22342-8)","DOI":"10.1007\/978-3-540-27813-9_6"},{"key":"288_CR31","unstructured":"Turing, A.M.: Checking a large routine. In: Report of a conference on high speed automatic calculating machines, pp. 67\u201369 (1948)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0288-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-013-0288-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-013-0288-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,3]],"date-time":"2022-03-03T18:03:59Z","timestamp":1646330639000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-013-0288-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,8,14]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2]]}},"alternative-id":["288"],"URL":"https:\/\/doi.org\/10.1007\/s10009-013-0288-8","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,8,14]]}}}