{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T14:08:00Z","timestamp":1746194880384},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642121883"},{"type":"electronic","value":"9783642121890"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12189-0_42","type":"book-chapter","created":{"date-parts":[[2010,3,31]],"date-time":"2010-03-31T22:11:05Z","timestamp":1270073465000},"page":"482-496","source":"Crossref","is-referenced-by-count":2,"title":["Termination of Loop Programs with Polynomial Guards"],"prefix":"10.1007","author":[{"given":"Bin","family":"Wu","sequence":"first","affiliation":[]},{"given":"Liyong","family":"Shen","sequence":"additional","affiliation":[]},{"given":"Zhongqin","family":"Bi","sequence":"additional","affiliation":[]},{"given":"Zhenbing","family":"Zeng","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"42_CR1","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science. Proceedings of Symposia in Applied Mathematics, vol.\u00a019, pp. 19\u201332. American Mathematical Socity (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"42_CR2","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of ACM"},{"issue":"2","key":"42_CR3","first-page":"230","volume":"42","author":"A. Turing","year":"1936","unstructured":"Turing, A.: On computable numbers, with an application to the entscheidungsproblem. London Mathematical Socity\u00a042(2), 230\u2013265 (1936)","journal-title":"London Mathematical Socity"},{"key":"42_CR4","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. Col\u00f3n","year":"2001","unstructured":"Col\u00f3n, M., Sipma, H.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"42_CR5","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. Col\u00f3n","year":"2002","unstructured":"Col\u00f3n, M., Sipma, H.: 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":"42_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"42_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1007\/11539452_37","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: Termination analysis of integer linear loops. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol.\u00a03653, pp. 488\u2013502. Springer, Heidelberg (2005)"},{"key":"42_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/b105073","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":"42_CR9","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":"42_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"42_CR11","first-page":"93","volume-title":"SEFM 2007: Software Engineering and Formal Methods","author":"D. Babic","year":"2007","unstructured":"Babic, D., Hu, A.J., Rakamaric, Z., Cook, B.: Proving termination by divergence. In: SEFM 2007: Software Engineering and Formal Methods, London, England, UK, pp. 93\u2013102. IEEE, Los Alamitos (2007)"},{"key":"42_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/11691372_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Leue","year":"2006","unstructured":"Leue, S., Wei, W.: A region graph based approach to termination proofs. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 318\u2013333. Springer, Heidelberg (2006)"},{"key":"42_CR13","doi-asserted-by":"publisher","first-page":"536","DOI":"10.1109\/ISCSCT.2008.58","volume-title":"ISCSCT 2008: International Symposium on Computer Science and Computational Technology","author":"B. Wu","year":"2008","unstructured":"Wu, B., Bi, Z.: Termination of nested loop. In: ISCSCT 2008: International Symposium on Computer Science and Computational Technology, Shanghai, China, vol.\u00a02, pp. 536\u2013539. IEEE, Los Alamitos (2008)"},{"key":"42_CR14","first-page":"32","volume-title":"LICS 2004: Logic in Computer Science","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS 2004: Logic in Computer Science, Turku, Finland, pp. 32\u201341. IEEE, Los Alamitos (2004)"},{"key":"42_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"42_CR16","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":"42_CR17","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1109\/ASEA.2008.18","volume-title":"ASEA 2008: Advanced Software Engineering and Its Applications","author":"Z. Bi","year":"2008","unstructured":"Bi, Z., Shan, M., Wu, B.: Non-termination analysis of linear loop programs with conditionals. In: ASEA 2008: Advanced Software Engineering and Its Applications, Hainan Island, China, pp. 159\u2013164. IEEE, Los Alamitos (2008)"},{"key":"42_CR18","volume-title":"Fixed Piont Theorems","author":"D.R. Smart","year":"1980","unstructured":"Smart, D.R.: Fixed Piont Theorems. Cambridge University Press, Cambridge (1980)"},{"key":"42_CR19","volume-title":"Linear algebra","author":"K. Hoffman","year":"1971","unstructured":"Hoffman, K., Kunze, R.: Linear algebra, 2nd edn. Prentice-Hall, New Jersey (1971)","edition":"2"},{"key":"42_CR20","unstructured":"Xia, B., Zhang, Z.: Termination of linear programs with nonlinear constraints (2009), \n                    \n                      http:\/\/arxiv.org\/abs\/0904.3588v1"}],"container-title":["Lecture Notes in Computer Science","Computational Science and Its Applications \u2013 ICCSA 2010"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12189-0_42.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:04:39Z","timestamp":1619784279000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12189-0_42"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642121883","9783642121890"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12189-0_42","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}