{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:56Z","timestamp":1725516536223},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_58","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"528-538","source":"Crossref","is-referenced-by-count":8,"title":["Program Verification by Using DISCOVERER"],"prefix":"10.1007","author":[{"given":"Lu","family":"Yang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bican","family":"Xia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chaochen","family":"Zhou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"3","key":"58_CR1","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/0304-3975(94)00202-T","volume":"138","author":"R. Alur","year":"1995","unstructured":"Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science\u00a0138(3), 3\u201334 (1995)","journal-title":"Theoretical Computer Science"},{"key":"58_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"58_CR3","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2005)"},{"issue":"2","key":"58_CR4","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clark","year":"1986","unstructured":"Clark, E.M., Emerson, A., Sistla, A.P.: Automatic verification of finite-state concurrent programs using temporal logic. ACM Transaction on Programming Languages and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"58_CR5","series-title":"Lecture Notes in Computer Science","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1981","unstructured":"Clarke, E.M., Emerson, E.A.: Synthesis of synchronization skeletons for branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, Springer, Heidelberg (1981)"},{"key":"58_CR6","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"58_CR7","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.) GI-Fachtagung 1975. LNCS, vol.\u00a033, pp. 134\u2013183. Springer, Heidelberg (1975)"},{"key":"58_CR8","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":"58_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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":"58_CR10","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":"58_CR11","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstraction interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: ACM POPL 1977, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"key":"58_CR12","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: ACM POPL 1979, pp. 269\u2013282 (1979)","DOI":"10.1145\/567752.567778"},{"key":"58_CR13","doi-asserted-by":"crossref","unstructured":"Damas, L., Milner, R.: Principal type-schemes for functional programs. In: ACM POPL 1982, pp. 207\u2013212 (1982)","DOI":"10.1145\/582153.582176"},{"key":"58_CR14","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":"58_CR15","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":"58_CR16","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1145\/333979.333989","volume":"4792","author":"R. Giacobazzi","year":"2000","unstructured":"Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretation complete. J. ACM\u00a04792, 361\u2013416 (2000)","journal-title":"J. ACM"},{"key":"58_CR17","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1006\/jcss.1998.1581","volume":"57","author":"T.A. Henzinger","year":"1998","unstructured":"Henzinger, T.A., Kopke, P.W., Puri, A., Varaiya, P.: What\u2019s decidable about hybrid automata? J. of Computer Science and System Sciences\u00a057, 94\u2013124 (1998)","journal-title":"J. of Computer Science and System Sciences"},{"key":"58_CR18","first-page":"1","volume":"11","author":"G. Lafferrierre","year":"2001","unstructured":"Lafferrierre, G., Pappas, G.J., Yovine, S.: Symbolic reachability computaion for families of linear vector fields. J. of Symbolic Computation\u00a011, 1\u201323 (2001)","journal-title":"J. of Symbolic Computation"},{"issue":"3","key":"58_CR19","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1016\/0022-0000(78)90014-4","volume":"17","author":"R. Milner","year":"1978","unstructured":"Milner, R.: A theory of polymorphism in programming. J. Computer System Science\u00a017(3), 348\u2013375 (1978)","journal-title":"J. Computer System Science"},{"key":"58_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction - CADE-11","author":"S. Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: A protype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol.\u00a0607, pp. 748\u2013752. Springer, Heidelberg (1992)"},{"issue":"5\/6","key":"58_CR21","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in the system Coq. J. Symbolic Logic\u00a015(5\/6), 607\u2013640 (1993)","journal-title":"J. Symbolic Logic"},{"key":"58_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/3-540-58179-0_46","volume-title":"Computer Aided Verification","author":"A. Puri","year":"1994","unstructured":"Puri, A., Varaiya, P.: Decidability of hybrid systems with rectangular differential inclusions. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 95\u2013104. Springer, Heidelberg (1994)"},{"key":"58_CR23","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":"58_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.-P. Queille","year":"1982","unstructured":"Queille, J.-P., Sifakis, J.: Verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"58_CR25","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"},{"key":"58_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"539","DOI":"10.1007\/978-3-540-24743-2_36","volume-title":"Hybrid Systems: Computation and Control","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Constructing invariants for hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol.\u00a02993, pp. 539\u2013554. Springer, Heidelberg (2004)"},{"key":"58_CR27","volume-title":"A Decision for Elementary Algebra and Geometry","author":"A. Tarski","year":"1951","unstructured":"Tarski, A.: A Decision for Elementary Algebra and Geometry, May 1951. University of California Press, Berkeley (1951)"},{"key":"58_CR28","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":"58_CR29","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1145\/1073884.1073933","volume-title":"Proceedings of the 2005 International Symposium on Symbolic and Algebraic Computation (ISSAC 2005)","author":"D. Wang","year":"2005","unstructured":"Wang, D., Xia, B.: Stability analysis of biological systems with real solution classification. In: Kauers, M. (ed.) Proceedings of the 2005 International Symposium on Symbolic and Algebraic Computation (ISSAC 2005), pp. 354\u2013361. ACM Press, New York (2005)"},{"key":"58_CR30","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":"58_CR31","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":"58_CR32","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":"58_CR33","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)"},{"issue":"12","key":"58_CR34","first-page":"897","volume":"10","author":"L. Yang","year":"2000","unstructured":"Yang, L., Xia, B.C.: An explicit criterion to determine the number of roots of a polynomial on an interval. Progress in Natural Science\u00a010(12), 897\u2013910 (2000)","journal-title":"Progress in Natural Science"},{"key":"58_CR35","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":"58_CR36","first-page":"110","volume-title":"Proceedings of International Workshop on Mathematics Mechanization 1992","author":"L. Yang","year":"1992","unstructured":"Yang, L., Zhang, J., Hou, X.: A criterion of dependency between algebraic equations and its applications. In: Wen-tsun, W., de Cheng, M.- (eds.) Proceedings of International Workshop on Mathematics Mechanization 1992, pp. 110\u2013134. International Academic Publishers, Beijing (1992)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_58","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T07:44:42Z","timestamp":1557733482000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_58"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_58","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}