{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,25]],"date-time":"2026-02-25T18:16:42Z","timestamp":1772043402900,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540752905","type":"print"},{"value":"9783540752929","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75292-9_3","type":"book-chapter","created":{"date-parts":[[2007,9,11]],"date-time":"2007-09-11T10:43:07Z","timestamp":1189507387000},"page":"34-49","source":"Crossref","is-referenced-by-count":28,"title":["Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems"],"prefix":"10.1007","author":[{"given":"Yinghua","family":"Chen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bican","family":"Xia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lu","family":"Yang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chaochen","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_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":"3_CR2","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. Bradley","year":"2005","unstructured":"Bradley, A., Manna, Z., Sipma, H.: Terminaition of polynomial programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 113\u2013129. Springer, Heidelberg (2005)"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: TERMINATOR: Beyond safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 415\u2013418. Springer, Heidelberg (2006)"},{"key":"3_CR4","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1016\/S0747-7171(08)80152-6","volume":"12","author":"G.E. Collins","year":"1991","unstructured":"Collins, G.E., Hong, H.: Partial cylindrical algebraic decomposition for quantifier elimination. J. of Symbolic Computation\u00a012, 299\u2013328 (1991)","journal-title":"J. of Symbolic Computation"},{"key":"3_CR5","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.B.: Synthesis of linear ranking functions. In: Margaria, T., Yi, W. (eds.) ETAPS 2001 and TACAS 2001. LNCS, vol.\u00a02031, pp. 67\u201381. Springer, Heidelberg (2001)"},{"key":"3_CR6","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, Langrangian Relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"3_CR7","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":"3_CR8","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Dolzman, A., Sturm, T.: REDLOG: Computer algebra meets computer logic. ACM SIGSAM Bulletin\u00a031(2), 2\u20139","DOI":"10.1145\/261320.261324"},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Proc. Symphosia in Applied Mathematics, vol.\u00a019, pp. 19\u201337 (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"issue":"10","key":"3_CR11","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. Comm. ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Comm. ACM"},{"key":"3_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, Heidelberg (1995)"},{"key":"3_CR13","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":"3_CR14","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: ACM POPL 2004, pp. 318\u2013329 (2004)","DOI":"10.1145\/964001.964028"},{"key":"3_CR15","volume-title":"A Decision for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"Tarski, A.: A Decision for Elementary Algebra and Geometry. University of California Press, Berkeley (1951)"},{"key":"3_CR16","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":"3_CR17","unstructured":"International Conference on Verified Software: Theories, Tools and Experiments, ETH Z\u00fcrich (October 10-13, 2005)"},{"key":"3_CR18","first-page":"207","volume":"4","author":"W.-T. Wu","year":"1984","unstructured":"Wu, W.-T.: Basic principles of mechanical theorem proving in elementary geometries. J. Syst. Sci. Math.\u00a04, 207\u2013235 (1984)","journal-title":"J. Syst. Sci. Math."},{"key":"3_CR19","unstructured":"Xia, B., Xiao, R., Yang, L.: Solving parametric semi-algebraic systems. In: Pae, S.-i., Park, H. (eds.) ASCM 2005. Proc. the 7th Asian Symposium on Computer Mathematics, Seoul, December 8-10, pp. 8\u201310 (2005)"},{"key":"3_CR20","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1006\/jsco.2002.0572","volume":"34","author":"B. Xia","year":"2002","unstructured":"Xia, B., Yang, L.: An algorithm for isolating the real solutions of semi-algebraic systems. J. Symbolic Computation\u00a034, 461\u2013477 (2002)","journal-title":"J. Symbolic Computation"},{"key":"3_CR21","doi-asserted-by":"publisher","first-page":"853","DOI":"10.1016\/j.camwa.2006.06.003","volume":"52","author":"B. Xia","year":"2006","unstructured":"Xia, B., Zhang, T.: Real Solution Isolation Using Interval Arithmetic. Comput. Math. Appl.\u00a052, 853\u2013860 (2006)","journal-title":"Comput. Math. Appl."},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1006\/jsco.1998.0274","volume":"28","author":"L. Yang","year":"1999","unstructured":"Yang, L.: Recent advances on determining the number of real roots of parametric polynomials. J. Symbolic Computation\u00a028, 225\u2013242 (1999)","journal-title":"J. Symbolic Computation"},{"key":"3_CR23","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/BF02713938","volume":"44","author":"L. Yang","year":"2001","unstructured":"Yang, L., Hou, X., Xia, B.: A complete algorithm for automated discovering of a class of inequality-type theorems. Sci. in China (Ser. F)\u00a044, 33\u201349 (2001)","journal-title":"Sci. in China (Ser. F)"},{"key":"3_CR24","first-page":"628","volume":"39","author":"L. Yang","year":"1996","unstructured":"Yang, L., Hou, X., Zeng, Z.: A complete discrimination system for polynomials. Science in China (Ser. E)\u00a039, 628\u2013646 (1996)","journal-title":"Science in China (Ser. E)"},{"key":"3_CR25","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1142\/9789812794833_0010","volume-title":"Geometric Computation","author":"L. Yang","year":"2004","unstructured":"Yang, L., Xia, B.: Automated Deduction in Real Geometry. In: Chen, F., Wang, D. (eds.) Geometric Computation, pp. 248\u2013298. World Scientific, Singapore (2004)"},{"key":"3_CR26","unstructured":"Yang, L., Xia, B.: Real solution classifications of a class of parametric semi-algebraic systems. In: Proc. of Int\u2019l Conf. on Algorithmic Algebra and Logic, pp. 281\u2013289 (2005)"},{"key":"3_CR27","doi-asserted-by":"crossref","unstructured":"Yang, L., Zhan, N., Xia, B., Zhou, C.: Program verification by using DISCOVERER. In: Proc. VSTTE 2005, Z\u00fcrich (October 10-October 13, 2005) (to appear)","DOI":"10.1007\/978-3-540-69149-5_58"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2007"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75292-9_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:59:00Z","timestamp":1619521140000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75292-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540752905","9783540752929"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75292-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}