{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:08:18Z","timestamp":1746194898550,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642329425"},{"type":"electronic","value":"9783642329432"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32943-2_5","type":"book-chapter","created":{"date-parts":[[2012,8,28]],"date-time":"2012-08-28T04:59:35Z","timestamp":1346129975000},"page":"61-73","source":"Crossref","is-referenced-by-count":3,"title":["Non-termination Sets of Simple Linear Loops"],"prefix":"10.1007","author":[{"given":"Liyun","family":"Dai","sequence":"first","affiliation":[]},{"given":"Bican","family":"Xia","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5_CR1","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":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/978-3-540-75292-9_3","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2007","author":"Y. Chen","year":"2007","unstructured":"Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol.\u00a04711, pp. 34\u201349. Springer, Heidelberg (2007)"},{"key":"5_CR3","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":"5_CR4","unstructured":"Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Workshop on Advances in Verification (WAVe 2000), pp. 1\u20138 (2000)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: POPL, pp. 81\u201392 (2001)","DOI":"10.1145\/373243.360210"},{"key":"5_CR6","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":"5_CR7","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":"5_CR8","doi-asserted-by":"publisher","first-page":"1234","DOI":"10.1016\/j.jsc.2010.06.006","volume":"45","author":"B. Xia","year":"2010","unstructured":"Xia, B., Zhang, Z.: Termination of linear programs with nonlinear constraints. Journal of Symbolic Computation\u00a045, 1234\u20131249 (2010)","journal-title":"Journal of Symbolic Computation"},{"key":"5_CR9","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s00165-009-0144-5","volume":"23","author":"B. Xia","year":"2011","unstructured":"Xia, B., Yang, L., Zhan, N., Zhang, Z.: Symbolic decision procedure for termination of linear programs. Formal Aspects of Computing\u00a023, 171\u2013190 (2011)","journal-title":"Formal Aspects of Computing"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Gupta, A., Henzinger, T., Majumdar, R., Rybalchenko, A., Xu, R.G.: Proving non-termination. In: POPL, pp. 147\u2013158 (2008)","DOI":"10.1145\/1328897.1328459"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: POPL, pp. 281\u2013292 (2008)","DOI":"10.1145\/1379022.1375616"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Zhao, S., Chen, D.: Decidability Analysis on Termination Set of Loop Programs. In: The International Conference on Computer Science and Service System(CSSS), pp. 3124\u20133127 (2011)","DOI":"10.1109\/CSSS.2011.5974588"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2012"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32943-2_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T10:33:24Z","timestamp":1744022004000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32943-2_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642329425","9783642329432"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32943-2_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}