{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:50:55Z","timestamp":1725490255904},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540752202"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75221-9_4","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T10:33:13Z","timestamp":1188469993000},"page":"67-82","source":"Crossref","is-referenced-by-count":24,"title":["Generating Polynomial Invariants with DISCOVERER and QEPCAD"],"prefix":"10.1007","author":[{"given":"Yinghua","family":"Chen","sequence":"first","affiliation":[]},{"given":"Bican","family":"Xia","sequence":"additional","affiliation":[]},{"given":"Lu","family":"Yang","sequence":"additional","affiliation":[]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/3-540-48294-6_4","volume-title":"Static Analysis","author":"F. Besson","year":"1999","unstructured":"Besson, F., Jensen, T., Talpin, J.-P.: Polyhedral analysis of synchronous languages. In: Cortesi, A., Fil\u00e9, G. (eds.) SAS 1999. LNCS, vol.\u00a01694, pp. 51\u201369. Springer, Heidelberg (1999)"},{"key":"4_CR2","doi-asserted-by":"crossref","unstructured":"Chen, Y., Xia, B., Yang, L., Zhan, N., Zhou, C.: Discovering non-linear ranking functions by solving semi-algebraic systems. In: ICTAC 2007. LNCS, Springer, Heidelberg (2007) (invited paper)","DOI":"10.1007\/978-3-540-75292-9_3"},{"key":"4_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/3-540-07407-4_17","volume-title":"Automata Theory and Formal Languages","author":"G.E. Collins","year":"1975","unstructured":"Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"4_CR4","doi-asserted-by":"crossref","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":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M. col\u00f3n","year":"2003","unstructured":"col\u00f3n, M., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"4_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":"4_CR7","doi-asserted-by":"crossref","unstructured":"Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among the variables of a program. In: ACM POPL 1978, pp. 84\u201397 (1978)","DOI":"10.1145\/512760.512770"},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0747-7171(88)80004-X","volume":"5","author":"J.H. Davenport","year":"1988","unstructured":"Davenport, J.H., Heintz, J.: Real Elimination is Doubly Exponential. J. of Symbolic Computation\u00a05, 29\u201337 (1988)","journal-title":"J. of Symbolic Computation"},{"key":"4_CR9","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":"4_CR10","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":"4_CR11","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"},{"key":"4_CR12","doi-asserted-by":"crossref","unstructured":"Gallo, G., Mishra, B.: Efficient Algorithms and Bounds for Wu-Ritt Characteristic Sets. In: Mora, T., Traverso, C. (eds.) Effective methods in algebraic geometry, Birkh\u00e4user, Bosten. Progress in Mathematics, pp. 119\u2013142 (1994)","DOI":"10.1007\/978-1-4612-0441-1_8"},{"issue":"1","key":"4_CR13","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1109\/TSE.1975.6312821","volume":"1","author":"S. German","year":"1975","unstructured":"German, S., Wegbreit, B.: A synthesizer of inductive assertions. IEEE Transactions on Software Engineering\u00a01(1), 68\u201375 (1975)","journal-title":"IEEE Transactions on Software Engineering"},{"issue":"10","key":"4_CR14","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":"4_CR15","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/BF00268497","volume":"6","author":"M. Karr","year":"1976","unstructured":"Karr, M.: Affine relationships among variables of a program. Acta Informatica\u00a06, 133\u2013151 (1976)","journal-title":"Acta Informatica"},{"issue":"4","key":"4_CR16","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1145\/360032.360048","volume":"19","author":"S. Katz","year":"1976","unstructured":"Katz, S., Manna, Z.: Logical analysis of programms. Communications of the ACM\u00a019(4), 188\u2013206 (1976)","journal-title":"Communications of the ACM"},{"key":"4_CR17","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier llimination. In: Proc. IMACS Intl. Conf. on Applications of Computer Algebra ( ACA 2004), Beaumont, Texas (July 2004)"},{"key":"4_CR18","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":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/3-540-45789-5_4","volume-title":"Static Analysis","author":"M. M\u00faller-Olm","year":"2002","unstructured":"M\u00faller-Olm, M., Seidl, H.: Polynomial constants are decidable. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol.\u00a02477, pp. 4\u201319. Springer, Heidelberg (2002)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"M\u00faller-Olm, M., Seidl, H.: Precise interprocedural analysis through linear algebra. In: ACM SIGPLAN Principles of Programming Languages, POPL 2004, pp. 330\u2013341 (2004)","DOI":"10.1145\/982962.964029"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/978-3-540-27864-1_21","volume-title":"Static Analysis","author":"E. Rodriguez-Carbonell","year":"2004","unstructured":"Rodriguez-Carbonell, E., Kapur, D.: An abstract interpretation approach for automatic generation of polynomial invariants. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol.\u00a03148, pp. 280\u2013295. Springer, Heidelberg (2004)"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Rodriguez-Carbonell, E., Kapur, D.: Automatic generation of polynomial loop invariants: algebraic foundations. In: Proc. Intl. Symp on Symbolic and Algebraic Computation (ISSAC 2004) (July 2004)","DOI":"10.1145\/1005285.1005324"},{"key":"4_CR23","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1016\/j.jsc.2007.01.002","volume":"42","author":"E. Rodriguez-Carbonell","year":"2007","unstructured":"Rodriguez-Carbonell, E., Kapur, D.: Generating all polynomial invariants in simple loops. Journal of Symbolic Computation\u00a042, 443\u2013476 (2007)","journal-title":"Journal of Symbolic Computation"},{"key":"4_CR24","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\/982962.964028"},{"issue":"2","key":"4_CR25","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1145\/360827.360850","volume":"17","author":"B. Wegbreit","year":"1974","unstructured":"Wegbreit, B.: The synthesis of loop predicates. Communications of the ACM\u00a017(2), 102\u2013112 (1974)","journal-title":"Communications of the ACM"},{"key":"4_CR26","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":"4_CR27","unstructured":"Xia, B., Xiao, R., Yang, L.: Solving parametric semi-algebraic systems. In: Pae, S.-l, Park, H. (eds.) Proc. the 7th Asian Symposium on Computer Mathematics (ASCM 2005), Seoul, December 8-10, pp. 153\u2013156 (2005)"},{"key":"4_CR28","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":"4_CR29","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":"4_CR30","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":"4_CR31","first-page":"33","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":"4_CR32","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":"4_CR33","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":"4_CR34","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)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Hybrid Real-Time Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75221-9_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:56:28Z","timestamp":1619520988000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75221-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540752202"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75221-9_4","relation":{},"subject":[]}}