基于符号计算方法的程序验证技术研究
|
摘要
程序验证是计算机程序设计领域的前沿研究课题,如何保证程序正确性是计算机科学的一个重大挑战.近年来,随着符号计算理论的不断完善和程序验证中使用精确无误差的数学方法的要求,使用符号计算理论来解决程序验证中的相关问题被认为是一种有效途径.本文利用符号计算的思想和方法研究了程序验证领域的三个基本问题：循环不变式生成、程序终止性分析以及前置条件生成.
循环不变式在程序的部分正确性验证中起着非常重要的作用,如何生成循环不变式也是程序验证领域的挑战之一.本文主要研究了多项式循环程序的不变式生成问题.首次将有限点集消去理想的思想和方法应用于多项式循环程序的不变式生成,设计了一个多项式时间复杂度的循环不变式自动生成算法,可生成多项式等式型循环不变式.
程序的终止性分析问题也是长期以来为众多计算机科学家所关注的问题之一.本文主要研究了一类带有非线性循环条件和线性赋值的循环程序的终止性分析问题.通过计算线性赋值矩阵的约当标准型,确定循环条件在循环次数充分大时的符号,将这类循环程序的终止性分析问题转化为判断参系数半代数系统有无实解的问题.如果参系数半代数系统中的左端函数个数有限或者左端函数都具有整数周期,则这类非线性循环程序的终止性问题是可判定的.
另外一个值得研究的问题是如何计算合理的前置条件,使得循环程序在满足该条件的前提下是终止的.本文基于一阶常系数差分方程组的求解技术,设计了一个高效、实用的前置条件生成算法.我们将程序的循环赋值语句转化为程序变量关于循环次数的差分方程组,计算差分方程组的闭形式解.然后将闭形式解代入循环条件,在循环次数充分大时,判断循环条件的符号,进而生成循环程序合理的前置条件.针对线性赋值程序给出了一个高效、实用的前置条件自动生成算法.进而,对于可求出闭形式解的非线性赋值循环程序以及运算可交换的多分支循环程序,也做了相应研究.
研究结果表明,符号计算是验证程序正确性的一种行之有效的方法.我们期待将符号计算中的一些经典算法更深入、广泛地应用到程序验证,并集成、研发新的有前途的验证工具.
Program verification is one of the frontier research topics in program design field, which has important theoretical significance and application value. In this dissertation, we introduce some classical algorithms in symbolic computation into program verification, and mainly do researches on program verification in three basic aspects:generation of program invariants, termination analysis and generation of preconditions.
Loop invariants play a very important role in proving partial correctness of pro-grams. we mainly study the invariant generation of polynomial loop programs. We firstly present a new method for generating polynomial invariants of polynomial loop programs by computing vanishing ideal of sampling points. A reliable polynomial time algorithm for generating polynomial invariants is established.
Termination analysis of loop programs is very important in many applications, es-pecially in those of safety critical software. In this dissertation, we mainly study the ter-mination of programs with polynomial guards and linear assignments. The discussion is based on simplifying the linear loops by its Jordan form. And then the process to find the nonterminating points for general polynomial guards be reduced to semi-algebraic system (SAS for short) solving. If the number of functions in SAS are finite or the functions are integer periodic, then the termination of programs is decidable.
However, instead of considering complete termination of programs, i.e., termination for all inputs, we are more concerned with the following questions:How if the code only terminates for some inputs? In this dissertation, a rapid and reliable algorithm for gener-ating preconditions of loop programs with linear or nonlinear assignments is established. Clearly, a loop program can be elegantly expressed by means of a system of difference equations, which describes the behavior of the loop variables changing at each iteration. The method is based on solving systems of difference equations corresponding to the loop assignments, and then substituting the solutions into the loop guards to compute precon-ditions that ensure the termination of the loop programs.
The results indicate that symbolic computation is a valid tool for studying program verification. We hope that more and more classical algorithms in symbolic computation can be introduced into research on program verification.
循环不变式在程序的部分正确性验证中起着非常重要的作用,如何生成循环不变式也是程序验证领域的挑战之一.本文主要研究了多项式循环程序的不变式生成问题.首次将有限点集消去理想的思想和方法应用于多项式循环程序的不变式生成,设计了一个多项式时间复杂度的循环不变式自动生成算法,可生成多项式等式型循环不变式.
程序的终止性分析问题也是长期以来为众多计算机科学家所关注的问题之一.本文主要研究了一类带有非线性循环条件和线性赋值的循环程序的终止性分析问题.通过计算线性赋值矩阵的约当标准型,确定循环条件在循环次数充分大时的符号,将这类循环程序的终止性分析问题转化为判断参系数半代数系统有无实解的问题.如果参系数半代数系统中的左端函数个数有限或者左端函数都具有整数周期,则这类非线性循环程序的终止性问题是可判定的.
另外一个值得研究的问题是如何计算合理的前置条件,使得循环程序在满足该条件的前提下是终止的.本文基于一阶常系数差分方程组的求解技术,设计了一个高效、实用的前置条件生成算法.我们将程序的循环赋值语句转化为程序变量关于循环次数的差分方程组,计算差分方程组的闭形式解.然后将闭形式解代入循环条件,在循环次数充分大时,判断循环条件的符号,进而生成循环程序合理的前置条件.针对线性赋值程序给出了一个高效、实用的前置条件自动生成算法.进而,对于可求出闭形式解的非线性赋值循环程序以及运算可交换的多分支循环程序,也做了相应研究.
研究结果表明,符号计算是验证程序正确性的一种行之有效的方法.我们期待将符号计算中的一些经典算法更深入、广泛地应用到程序验证,并集成、研发新的有前途的验证工具.
Program verification is one of the frontier research topics in program design field, which has important theoretical significance and application value. In this dissertation, we introduce some classical algorithms in symbolic computation into program verification, and mainly do researches on program verification in three basic aspects:generation of program invariants, termination analysis and generation of preconditions.
Loop invariants play a very important role in proving partial correctness of pro-grams. we mainly study the invariant generation of polynomial loop programs. We firstly present a new method for generating polynomial invariants of polynomial loop programs by computing vanishing ideal of sampling points. A reliable polynomial time algorithm for generating polynomial invariants is established.
Termination analysis of loop programs is very important in many applications, es-pecially in those of safety critical software. In this dissertation, we mainly study the ter-mination of programs with polynomial guards and linear assignments. The discussion is based on simplifying the linear loops by its Jordan form. And then the process to find the nonterminating points for general polynomial guards be reduced to semi-algebraic system (SAS for short) solving. If the number of functions in SAS are finite or the functions are integer periodic, then the termination of programs is decidable.
However, instead of considering complete termination of programs, i.e., termination for all inputs, we are more concerned with the following questions:How if the code only terminates for some inputs? In this dissertation, a rapid and reliable algorithm for gener-ating preconditions of loop programs with linear or nonlinear assignments is established. Clearly, a loop program can be elegantly expressed by means of a system of difference equations, which describes the behavior of the loop variables changing at each iteration. The method is based on solving systems of difference equations corresponding to the loop assignments, and then substituting the solutions into the loop guards to compute precon-ditions that ensure the termination of the loop programs.
The results indicate that symbolic computation is a valid tool for studying program verification. We hope that more and more classical algorithms in symbolic computation can be introduced into research on program verification.
引文
[1]http://research.microsoft.com/TERMINATOR.
[2]http://theory.stanford.edu/srirams/Software/sting.html.
[3]http://www-spiral.lip6.fr/wang/epsilon/.
[4]http://www.astree.ens.fr/.
[5]http://www.is.pku.edu.cn/-xbc/software.html.
[6]http://www.maplesoft.com.
[7]http://www.mmrc.iss.ac.cn/mmp/.
[8]http://www.mpi-inf.mpg.de/rybal/rankfinder/.
[9]http://www.risc.uni-linz.ac.at/research/theorema.
[10]http://www.singular.uni-kl.de/.
[11]http://www.wolfram.com/products/mathematica/index.html.
[12]高小山,王定康,裘宗燕,杨宏.方程求解与机器证明.科学出版社,北京,2006.
[13]杨路,张景中,侯晓荣.非线性代数方程组与定理机器证明.上海科技教育出版社,上海,1996.
[14]杨路,候晓荣,曾振柄.多项式的完全判别系统.中国科学(E),26：424-441,1996.
[15]符红光,杨路,曾振柄.构造广义sturm序列的递归算法.中国科学(E),29：546-555,1999.
[16]王东明,杨路,李志斌.符号计算选讲.清华大学出版社,2003.
[17]王东明,夏壁灿,李子明.计算机代数.清华大学出版社,2006.
[18]吴顺堂,邓之光.有限差分方程概论.河海大学出版社,1993.
[19]张景中,梁松新.复系数多项式完全判别系统及其自动生成.中国科学(E),29：61-75，1999.
[20]杨路,夏壁灿.不等式机器证明与自动发现.科学出版社,北京,2008.
[21]吴文俊.复兴构造性的数学.数学进展,(14)：334-339,1985.
[22]张景中.计算机怎样解几何题.暨南大学出版社,广州,2000.
[23]刘木兰.Grobner基理论及其应用.科学出版社,2000.
[24]王东明.消去法及其应用.科学出版社,北京,2002.
[25]李大潜.谈谈现代应用数学.中国科学院院刊,(18)：219-222,2003.
[26]杨德庄.灵活的数学技术.数学进展,(34)：1-16,2005.
[27]陈应华.用实代数方法寻找不变量和秩函数.Master's thesis,北京大学,北京,2007.
[28]毕忠勤.基于实代数符号计算的程序验证技术研究.PhD thesis,华东师范大学,上海,2009.
[29]Building a better bug-trap. Economist Magazine, June 2003.
[30]John Abbott, Anna Maria Bigatti, Martin Kreuzer, and Lorenzo Robbiano. Com-puting ideals of points. Journal of Symbolic Computation,30(4):341-356,2000.
[31]William W. Adams and Philippe Loustaunau. An Introduction to Grobner Bases. American Mathematical Society,1994.
[32]Rajeev Alur and Thomas A. Henzinger. Real-time logics:Complexity and expres-siveness. In LICS'1990:Fifth Annual IEEE Symposium on Logic in Computer Science, pages 390-401, Philadelphia, Pennsylvania, USA,1990. IEEE Computer Society.
[33]Krzysztof R. Apt and Ernst-Rudiger Olderog. Verification of Sequential and Con-current Programs. Springer-Verlag,2nd edition,1997.
[34]Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, and Byron Cook. Proving termi-nation by divergence. In SEFM'2007:Software Engineering and Formal Methods, pages 93-102, London, England, UK,2007. IEEE COMPUTER SOCIETY.
[35]Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter W. O'Hearn. Variance analyses from invariance analyses. In Martin Hofmann and Matthias Felleisen, editors, POPL'2007:Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 211-224, Nice, France,2007. ACM Press.
[36]Josh Berdine, Byron Cook, Dino Distefano, and Peter W. O'Hearn. Automatic termination proofs for programs with shape-shifting heaps. In Thomas Ball and Robert B. Jones, editors, CAV'2006:Computer Aided Verification, volume 4144 of LNCS, pages 386-400, Seattle, WA, USA,2006. Springer-Verlag.
[37]Zhongqin Bi, Meijing Shan, and Bin Wu. Non-termination analysis of linear loop programs with conditionals. In ASEA'2008:Advanced Software Engineering and Its Applications, pages 159-164, Hainan Island, China,2008. IEEE COMPUTER SOCIETY.
[38]Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Linear ranking with reach-ability. In CAV'2005:Computer Aided Verification, volume 3576 of LNCS, pages 491-504, Edinburgh, Scotland, UK,2005. Springer-Verlag.
[39]Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Termination analysis of integer linear loops. In CONCUR'2005:Concurrency Theory,16th International Conference, volume 3653 of LNCS, pages 488-502, San Francisco, CA, USA, 2005. Springer-Verlag.
[40]Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Termination of polynomial programs. In Radhia Cousot, editor, VMCAI'2005:Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS, pages 113-129, Paris, Frence, 2005. Springer-Verlag.
[41]Mark Braverman. Termination of integer linear programs. In Thomas Ball and Robert B. Jones, editors, CAV'2006:Computer Aided Verification, volume 4144 of LNCS, pages 372-385, Seattle, WA, USA,2006. Springer-Verlag.
[42]Bruno Buchberger. An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal. PhD thesis, Mathemat-ical Institue, University of Innsbruck, Austria,1965.
[43]Bruno Buchberger. An algorithmical criterion for the solvability of algebraic sys-tems of equations. Aequationes Mathematicae,4(3):374-383,1970.
[44]Bruno Buchberger. Grobner-Bases:An Algorithmic Method in Polynomial Ideal Theory. Reidel Publishing Company, Dodrecht-Boston-Lancaster,1985.
[45]Bruno Buchberger. Practical and theoretical aspects of program verification. In Computer Aided Verification of Information Systems, Romanian-Austrian Work-shop, Timisoara, Romania, February 2003.
[46]Bruno Buchberger and Franz Lichtenberger. Mathematik furInformatiker I:Die Methode der Mathematik. Springer-Verlag, New York,1981.
[47]Tevfik Bultan, Richard Gerber, and William Pugh. Symbolic model checking of infinite state systems using presburger arithmetic. In Orna Grumberg, editor, CAV'1997:Computer Aided Verification, volume 1254 of LNCS, pages 400-411, Haifa, Israel,1997. Springer-Verlag.
[48]Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Foot-print analysis:A shape analysis that discovers preconditions. In Hanne Riis Niel-son and Gilberto File, editors, SAS'2007:Static Analysis,14th International Sym-posium, volume 4634 of LNCS, pages 402-418, Kongens Lyngby, Denmark,2007. Springer-Verlag.
[49]Georg Cantor. Contributions to the Founding of the Theory of Transfinite Num-bers. Dover, New York,1955.
[50]Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang. Ranking abstractions. In Sophia Drossopoulou, editor, ESOP'2008:17th European Symposium on Programming, volume 4960 of LNCS, pages 148-162, Budapest, Hungary,2008. Springer-Verlag.
[51]Changbo Chen, Marc Moreno Maza, Bican Xia, and Lu Yang. Computing cylin-drical algebraic decomposition via triangular decomposition. In Jeremy Johnson, Hyungju Park, and Erich Kaltofen, editors, ISSAC'2009:International Sympo-sium on Symbolic and Algebraic Computation, pages 95-102, Seoul, Korea,2009. ACM Press.
[52]Falai Chen, Jiansong Deng, and Yuyu Feng. Algebraic surface blending using wu's method. In Xiao shan Gao and Dongming Wang, editors, ASCM'2000: COMPUTER MATHEMATICS:Proceedings of 4th Asian Symposium on Com-puter Mathematics, volume 8, pages 172-181, Chiang Mai, Thailand,2000. World Scientific.
[53]William Y. C. Chen. A general bijective algorithm for increasing tress. Systems Science and Mathematical Sciences,12:193-203,1999.
[54]Yinghua Chen, Bican Xia, Lu Yang, and Naijun Zhan. Generating polynomial invariants with discoverer and qepcad. In C. B. Jones, Z. Liu, and J. Woodcock, editors, Fonnal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pages 67-82, Macao China. Springer-Verlag.
[55]Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, and Chaochen Zhou. Discov-ering non-linear ranking functions by solving semi-algebraic systems. In Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors, ICTAC'2007:Theoretical As-pects of Computing, volume 4711 of LNCS, pages 34-49, Macau, China,2007. Springer-Verlag.
[56]George E. Collins. Hauptvortrag:Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, volume 33 of LNCS, pages 134-183, London, UK,1975. Springer-Verlag.
[57]George E. Collins and Hoon Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation,12(3):299-328,1991.
[58]Michael Colon, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. In Warren A. Hunt Jr. and Fabio Somenzi, editors, CAV'2003:Computer Aided Verification, volume 2725 of LNCS, pages 420-432, Chicago, IL, USA,2003. Springer-Verlag.
[59]Michael Colon and Henny Sipma. Synthesis of linear ranking functions. In Tiziana Margaria and Wang Yi, editors, TACAS'2001, Tools and Algorithms for the Con-struction and Analysis of Systems, volume 2031 of LNCS, pages 67-81, Italy, 2001. Springer-Verlag.
[60]Michael Colon and Henny Sipma. Practical methods for proving program termina-tion. In Ed Brinksma and Kim Guldstrand Larsen, editors, CAV'2002:Computer Aided Verification, volume 2404 of LNCS, pages 442-454, Copenhagen, Den-mark,2002. Springer-Verlag.
[61]Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Y. Vardi. Proving that programs eventually do something good. In Mar-tin Hofmann and Matthias Felleisen, editors, POPL'2007:Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 265-276, Nice, France,2007. ACM Press.
[62]Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sa-giv. Proving conditional termination. In Aarti Gupta and Sharad Malik, editors, CAV'2008:Computer Aided Verification, volume 5123 of LNCS, pages 328-340, Princeton, NJ, USA,2008. Springer-Verlag.
[63]Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Abstraction refinement for termination. In Chris Hankin and Igor Siveroni, editors, SAS'2005:Static Analysis, volume 3672 of LNCS, pages 87-101, London, UK,2005. Springer-Verlag.
[64]Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination proofs for systems code. In Michael I. Schwartzbach and Thomas Ball, editors, PLDI'2006: Conference on Programming Language Design and Implementation, pages 415-426, Ottawa, Ontario, Canada,2006. ACM Press.
[65]Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Terminator:Beyond safety. In Thomas Ball and Robert B. Jones, editors, CAV'2006:Computer Aided Verification, volume 4144 of LNCS, pages 415-418, Seattle, WA, USA,2006. Springer-Verlag.
[66]Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving thread termina-tion. In Jeanne Ferrante and Kathryn S. McKinley, editors, PLDI'2007:Proceed-ings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pages 320-330, San Diego, California, USA,2007. ACM Press.
[67]Patrick Cousot. Proving program invariance and termination by parametric ab-straction, lagrangian relaxation and semidefinite programming. In Radhia Cousot, editor, VMCAI'2005:Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS, pages 1-24, Paris, France,2005. Springer-Verlag.
[68]Patrick Cousot and Radhia Cousot. Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'1977:Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238-252, Los Ange-les, California,1977. ACM Press, New York, NY.
[69]Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming,13(2-3):103-179,1992.
[70]Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL'1978:Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 84-96, Tucson, Arizona,1978. ACM Press, New York, NY.
[71]David A. Cox, John B. Little, and Donal O'Shea. Ideals, Varieties, and Algo-rithms:An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer-Verlag,2005.
[72]David A. Cox, John B. Little, and Donal O'Shea. Using Algebraic Geometry. Springer-Verlag,2nd edition,2005.
[73]Paul Cull, Mary Flahive, and Robby Robson. Difference Equations:From Rabbits to Chaos. Springer,2005.
[74]David Delmas and Jean Souyris. Astree:From research to industry. In Hanne Riis Nielson and Gilberto File, editors, SAS'2007:14th International Symposium on Static Analysis, volume 4634 of LNCS, pages 437-451, Kongens Lyngby,2007. Springer-Berlin.
[75]Edsger W. Dijkstra. Notes on structured programming. In O.-J. Dahl, E. W. Dijk-stra, and C. A. R. Hoare, editors, Structured Programming, London,1972. Aca-demic Press.
[76]Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall Inc, New Jersey, 1976.
[77]Edsger W. Dijkstra and Carel S. Scholten. Predicate calculus and program seman-tics. Springer-Verlag, New York,1990.
[78]Saber Elaydi. An Introduction to Difference Equations. Springer, New York,3rd edition,2005.
[79]Julius Farkas. Uber die theorie der einfachen ungleichungen. Journal fur die Reine und Angewandte Mathematik,124:1-27.
[80]Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Math-ematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19-32, Providence, Rhode Island,1967. American Mathematical Socity.
[81]Ralf Froberg. An Introduction to Grobner Bases. John Wiley & Sons,1998.
[82]Gerald Futschek. Programmentwicklung und Verifikation. Springer-Verlag, Wien, New York,1989.
[83]Steven M. German and Ben Wegbreit. A synthesizer of inductive assertions. IEEE Transactions on Software Engineering,1(1):68-75,1975.
[84]David Gries. The Science of Programming. Springer-Verlag, New York,1981.
[85]Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. Program anal-ysis as constraint solving. In Rajiv Gupta and Saman P. Amarasinghe, editors, PLDI'2008:Proceedings of the ACM SIGPLAN 2008 Conference on Program-ming Language Design and Implementation, volume 43, pages 281-292, Tucson, AZ, USA,2008. ACM.
[86]A. Gupta, T. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu. Proving non-termination. In George C. Necula and Philip Wadler, editors, POPL'2008:Princi-ples of programming languages, pages 147-158, San Francisco, California, USA, 2008. ACM Press.
[87]Venkatesan Guruswami and Madhu Sudan. Improved decoding of reed-solomon and algebraic-geometry codes. IEEE Transactions on Information Theory, 45(6):1757-1767,1999.
[88]Thomas A. Henzinger and Pei-Hsin Ho. Algorithmic analysis of nonlinear hy-brid systems. In Pierre Wolper, editor, CAV'1995:Computer Aided Verification, volume 939 of LNCS, pages 225-238, Liege, Belgium,1995. Springer-Verlag.
[89]Heisuke Hironaka. The resolution of singularities of an algebraic variety over a field of characteristic zero. Annals of Mathematics,79:109-326,1964.
[90]C. A. R. Hoare. An axiomatic basis for computer programming. Communications of ACM,12(10):576-580, October 1969.
[91]Tony Hoare. The verifying compiler:A grand challenge for computing research. Journal of the ACM,50(1):63-69,2003.
[92]K. Hoffman and R. Kunze. Linear algebra. Prentice-Hall, New Jersey,2n edition, 1971.
[93]Peter Vincent Homeier. Trustworthy Tools for Trustworthy Programs:A Me-chanically Verified Verification Condition Generator for the Total Correctness of Procedures. PhD thesis, Universitiy of California,1995.
[94]Charles Jordan. Calculus of Finite Difference. Chelsea Publishing Company, New York,3rd edition,1965.
[95]Erich Kaltofen and Zhengfeng Yang. On exact and approximate interpolation of sparse rational functions. In Dongming Wang, editor, ISSAC'2007:International Symposium on Symbolic and Algebraic Computation, pages 203-210, Waterloo, Ontario, Canada,2007. ACM Press.
[96]Deepak Kapur. Automatically generating loop invariants using quantifier elimina-tion. In ACA'04:Proc. IMACS Intl. Conf. on Applications of Computer Algebra, Beaumont, Texas,2004.
[97]Deepak Kapur and Joseph L. Mundy. Wu's method and its application to perspec-tive viewing. Artificial Intelligence,37(1-3):15-36,1988.
[98]Michael Karr. Affine relationships among variables of a program. Acta Informat-ica,6:133-151,1976.
[99]Shmuel Katz and Zohar Manna. Logical analysis of programs. Communications of ACM,19(4):188-206,1976.
[100]Manuel Kauers and Burkhard Zimmermann. Computing the algebraic relations of c-finite sequences and multisequences. Journal of Symbolic Computation, 43(11):787-803,2008.
[101]Martin Kirchner. Program verification with the mathematical software system Theorema. PhD thesis, Research Institute for Symbolic Computation, Johannes Kepler University of Linz, Austria,1999.
[102]Ralf Koetter and Alexander Vardy. Algebraic soft-decision decoding of reed-solomon codes. IEEE Transactions on Information Theory,49(11):2809-2825, 2003.
[103]Laura Ildiko Kovacs. Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. PhD thesis, Research Institute for Symbolic Computation, Johannes Kepler University of Linz, Austria,2007.
[104]Laura Ildiko Kovacs. Reasoning algebraically about p-solvable loops. In C. R. Ramakrishnan and Jakob Rehof, editors, TACAS'2008:Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 249-264, Budapest, Hungary,2008. Springer-Verlag.
[105]Laura Ildiko Kovacs and Tudor Jebelean. Automated generation of loop invariants by recurrence solving in theorema. Annals of the West University of Timisoara. Series Mathematics-Computer Science, XLⅡ:151-166,2004. Special issue on Computer Science-Proceedings of SYNASC'04.
[106]Laura Ildiko Kovacs and Tudor Jebelean. Generation of loop invariants in the-orema by combinatorial and algebraic methods. Bulletins for Applied and Com-puter Mathematics, CVI(2172):125-134,2004. Proceedings of Pannonian Applied Mathematical Meetings, PC-144.
[107]Laura Ildiko Kovacs and Tudor Jebelean. An algorithm for automated generation of invariants for loops with conditionals. In SYNASC'2005:Proceedings of the Seventh International Symposium on Symbolic and Numeric Algorithms for Sci-entific Computing, pages 245-249. IEEE Computer Society,2005.
[108]Laura Ildiko Kovacs and Tudor Jebelean. Finding polynomial invariants for im-perative loops in the theorema system. In Proceeding of Verify 2006 Workshop, pages 52-67,2006.
[109]Gerardo Lafferriere, George J. Pappas, and Shankar Sastry.0-minimal hybrid systems. Mathematics of Control, Signals, and Systems,13:1-21,2000.
[110]Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. Symbolic reachability computation for families of linear vector fields. Journal of Symbolic Computation, 32(3):231-253,2001.
[111]Reinhard Laubenbacher and Brandilyn Stigler. A computational algebra approach to the reverse engineering of gene regulatory networks. Journal of Theoretical Biology,229:523-537,2004.
[112]K. Rustan M. Leino. Efficient weakest preconditions. Information Processing Letters,93(6):281-288,2005.
[113]Stefan Leue and Wei Wei. A region graph based approach to termination proofs. In Holger Hermanns and Jens Palsberg, editors, TACAS'2006:Tools and Algorithms for the Construction and Analysis of Systems, volume 3920 of LNCS, pages 318-333, Vienna, Austria,2006. Springer-Verlag.
[114]Hongbo Li. Clifford algebra approaches to mechanical geometry theorem proving. In Xiao-Shan Gao and Dongming Wang, editors, Mathematics Mechanication, pages 205-229, London, UK,2000. Academic Press.
[115]Stephen Magill, Josh Berdine, Edmund M. Clarke, and Byron Cook. Arithmetic strengthening for shape analysis. In Hanne Riis Nielson and Gilberto File, editors, SAS'2007:Static Analysis,14th International Symposium, volume 4634 of LNCS, pages 419-436, Kongens Lyngby, Denmark,2007. Springer-Verlag.
[116]Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York,1995.
[117]M. G. Marinari, H. Michael Moller, and T. Mora. Grobner bases of ideals de-fined by functionals with an application to ideals of projective points. Applicable Algebra in Engineering, Communication and Computing,4(2):103-145,1993.
[118]Richard K. Miller and Anthony N. Michel. Ordinary differential equations. Aca-demic Press, New York,1982.
[119]H. Michael Moller and Bruno Buchberger. The construction of multivariate poly-nomials with preassigned zeros. In Jacques Calmet, editor, EUROCAM'1982:Eu-ropean Computer Algebra Conference, volume 144 of LNCS, pages 24-31, Mar-seille, France,1982. Springer, Berlin-New York.
[120]Markus Muller-Olm, Michael Petter, and Helmut Seidl. Interprocedurally ana-lyzing polynomial identities. In Bruno Durand and Wolfgang Thomas, editors, STACS'2006:23rd Annual Symposium on Theoretical Aspects of Computer Sci-ence, volume 3884 of LNCS, pages 50-67, Marseille, France,2006. Springer-Verlag.
[121]Markus Muller-Olm and Helmut Seidl. Polynomial constants are decidable. In Manuel V. Hermenegildo and German Puebla, editors, SAS'2002:Static Analysis, 9th International Symposium, volume 2477 of LNCS, pages 4-19, Madrid, Spain, 2002. Springer-Verlag.
[122]Markus Muller-Olm and Helmut Seidl. Computing polynomial program invariants. Information Processing Letters,91(5):233-244,2004.
[123]Markus Muller-Olm and Helmut Seidl. A note on karr's algorithm. In Josep Diaz, Juhani Karhumaki, Arto Lepisto, and Donald Sannella, editors, ICALP'2004: 31st International Colloquium on Automata, Languages and Programming, vol-ume 3142 of LNCS, pages 1016-1028, Turku, Finland,2004. Springer-Verlag.
[124]Markus Muller-Olm and Helmut Seidl. Precise interprocedural analysis through linear algebra. In POPL'2004:Proceedings of the 31 st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 330-341, Venice, Italy, 2004. ACM Press, New York, NY.
[125]Michael Petter. Berechnung von polynomiellen invarianten. Master's thesis, Fakultat fur Informatik, Technische Universitat Munchen, Austria,2004.
[126]Giovanni Pistone, Eva Riccomagno, and Henry P. Wynn. Algebraic Statistics: Computational Commutative Algebra in Statistics. Monographs on Statistics & Applied Probability. Chapman & Hall/CRC,2001.
[127]Andreas Podelski and Andrey Rybalchenko. A complete method for the synthe-sis of linear ranking functions. In Bernhard Steffen and Giorgio Levi, editors, VMCAI'2004:Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS, pages 239-251, Venice, Italy,2004. Springer-Verlag.
[128]Enric Rodriguez-Carbonell and Deepak Kapur. Automatic generation of polyno-mial loop invariants:Algebraic foundations. In ISSAC'2004:Proceedings of the 2004 international symposium on Symbolic and algebraic computation, pages 266-273, Santander, Spain,2004. ACM Press, New York, NY.
[129]Enric Rodriguez-Carbonell and Deepak Kapur. Generating all polynomial invari-ants in simple loops. Journal of Symbolic Computation,42(4):443-476,2007.
[130]Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Petri net analysis using invariant generation. In Nachum Dershowitz, editor, Verification:Theory and Practice 2003, volume 2772 of LNCS, pages 682-701. Springer-Verlag,2003.
[131]Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Constructing in-variants for hybrid systems. In Rajeev Alur and George J. Pappas, editors, HSCC'2004:7th International Workshop on Hybrid Systems:Computation and Control, volume 2993 of LNCS, pages 539-554, Philadelphia, PA, USA,2004. Springer-Verlag.
[132]Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Constraint-based linear-relations analysis. In Roberto Giacobazzi, editor, SAS'2004:11th Inter-national Symposium on Static Analysis, volume 3148 of LNCS, pages 53-68, Verona, Italy,2004. Springer.
[133]Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Non-linear loop invariant generation using grobner bases. In POPL'2004:Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 318-329, Venice, Italy,2004. ACM Press, New York, NY.
[134]Alexander Schrijver. Theory of Linear and Integer Programming. Wiley, John & Sons,1986.
[135]Jacob T. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. Journal of the ACM,27(4):701-717,1980.
[136]Liyong Shen, Min Wu, Zhengfeng Yang, and Zhenbing Zeng. Finding positively invariant sets of a class of nonlinear loops via curve fitting. In SNC'09:Proceed- ings of the 2009 conference on Symbolic numeric computation, pages 185-190, Kyoto, Japan,2009. ACM Press.
[137]D.R. Smart. Fixed Piont Theorems. Cambridge University Press,1980.
[138]Gary Stix. Send in the terminator:A microsoft tool looks for programs that freeze up. Scientific American Magazine, November 2006.
[139]Christopher Strachey. An impossible program. Computer Journal,7(4):313,1965.
[140]Madhu Sudan. Decoding of reed solomon codes beyond the error-correction bound. Journal of Complexity,13(1):180-193,1997.
[141]Ashish Tiwari. Termination of linear programs. In Rajeev Alur and Doron Peled, editors, CAV'2004:Computer Aided Verification, volume 3114 of LNCS, pages 70-82, Boston, MA, USA,2004. Springer-Verlag.
[142]Ashish Tiwari. An algebraic approach for the unsatisfiability of nonlinear con-straints. In C.-H. Luke Ong, editor, CSL'2005:19th International Workshop on Computer Science Logic, volume 3634 of LNCS, pages 248-262, Oxford, UK, 2005. Springer-Berlin.
[143]Ashish Tiwari and Gaurav Khanna. Series of abstractions for hybrid automata. In Claire Tomlin and Mark R. Greenstreet, editors, HSCC'2002:Hybrid Systems: Computation and Control, volume 2289 of LNCS, pages 465-478, Stanford, CA, USA,2002. Springer-Berlin.
[144]Ashish Tiwari, Harald RueB, Hassen Saidi, and Natarajan Shankar. A technique for invariant generation. In Tiziana Margaria and Wang Yi, editors, TACAS'2001: 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of LNCS, pages 113-127, Genova, Italy,2001. Springer-Verlag.
[145]Alan Turing. On computable numbers, with an application to the entschei-dungsproblem. London Mathematical Socity,42(2):230-265,1936.
[146]Joachim von zur Gathen and Jurgen Gerhard. Modern Computer Algebra. Cam-bridge University Press,2nd edition,2003.
[147]Dongming Wang. Elimination Practice:Software Tools and Applications. Impe-rial College Press, London,2004.
[148]Ben Wegbreit. The synthesis of loop predicates. Communications of ACM, 17(2):102-112,1974.
[149]Ben Wegbreit. Property extraction in well-founded property set. IEEE Transac-tions on Software Engineering, 1(3):270-9285,1975.
[150]Volker Weispfenning. Quantifier elimination for real algebra-the quadratic case and beyond. Applicable Algebra in Engineering, Communication and Computing, 8(2):85-101,1997.
[151]Jinzhao Wu and Zhuojun Liu. Well-behaved inference rules for first-order theorem proving. Journal of Automated Reasoning,21(3):381-400,1998.
[152]Wen-Tsun Wu. A mechanization method of geometry and its applications iv. some theorems in planar kinematics. System Science and Mathematical Scienc, (2):97-109,1989.
[153]Wen-Tsun Wu. On the chemical equlibrium problem and equation-solving. Acta Mathematica Sinica, (10):361-374,1990.
[154]Wen-Tsun Wu. Mechanical theorem proving of differential geometries and some of its applications in mechanics. Journal of Automated Beasoning, (7):171-191, 1991.
[155]Wen-Tsun Wu. Mathematics Mechanization:Mechanical Geometry Theorem-Proving, Mechanical Geometry Problem-Solving, and Polynomial Equations-Solving. Kluwer Academic Publishers, Norwell, MA, USA,2001.
[156]Bican Xia. Discoverer:A tool for solving problems involving polynomial inequal-ities. In et al Yang W-C, editor, ATCM'2000:5th Asian Technology Conference in Mathematics, pages 472-481, Chiang Mai, Thailand,2000.
[157]Bican Xia, Rong Xiao, and Lu Yang. Solving parametric semi-algebraic systems. In Sung il Pae and H. Park, editors, ACSM'2005:7th Asian Symposium on Com-puter Mathematics, pages 153-156, Seoul, Korea,2005.
[158]Bican Xia and Lu Yang. An algorithm for isolating the real solutions of semi-algebraic systems. Journal of Symbolic Computation,34(5):461-477,2002.
[159]Bican Xia, Lu Yang, and Naijun Zhan. Program verification by reduction to semi-algebraic systems solving. In Tiziana Margaria and Bernhard Steffen, editors, ISoLA'2008:Leveraging Applications of Formal Methods, Verification and Val-idation, volume 17 of Communications in Computer and Information Science, pages 277-291, Porto Sani, Greece,2008. Springer-Verlag.
[160]Bican Xia, Lu Yang, Naijun Zhan, and Zhihai Zhang. Symbolic decision procedure for termination of linear programs. to appear in Formal Aspects of Computing.
[161]Lu Yang. Practical automated reasoning on inequalities:Generic programs for inequality proving and discovering. In Wei-Chi Yang, Kiyoshi Shirayanagi, Sung-Chi Chu, and Gary Fitz-Gerald, editors, ATCM'1998:Asian Technology Confer-ence in Mathematics, pages 24-35, Tsukuba, Japan,1998. Springer-Verlag.
[162]Lu Yang. Recent advances in automated theorem proving on inequalities. Journal of Computer Science and Technology,14(5):434-446,1999.
[163]Lu Yang. Recent advances on determining the number of real roots of parametric polynomials. Journal of Symbolic Computation,28(1-2):225-242,1999.
[164]Lu Yang and Bican Xia. Real solution classifications of a class of parametric semi-algebraic systems. In A. Dolzmann, A. Seidl, and T. Sturm, editors, A3L'2005: Algorithmic Algebra and Logic, pages 281-289,2005.
[165]Lu Yang and Shihong Xia. An inequality-proving program applied to global op-timization. In Wei-Chi Yang, Sung-Chi Chu, and Jen-Chung Chuan, editors, ATCM'2000:Asian Technology Conference in Mathematics, pages 40-51, Chi-ang Mai, Thailand,2000.
[166]Lu Yang, Naijun Zhan, Bican Xia, and Chaochen Zhou. Program verification by using discoverer. In Bertrand Meyer and Jim Woodcock, editors, VSTTE'2005: Verified Software:Theories, Tools, Experiments, volume 4171 of LNCS, pages 528-538, Zurich, Switzerland,2005. Springer-Verlag.
[167]Lu Yang and Jingzhong Zhang. A practical program of automated proving for a class of geometric inequalities. In ADG'00:3rd International Workshop on Automated Deduction in Geometry, pages 41-57, London, UK,2000. Springer-Verlag.
[168]Lu Yang, Jingzhong Zhang, and Weinian Zhang. On number of circles intersected by a line. Journal of Combinatorial Theory(Series A),98(2):395-405,2002.
[169]Lu Yang, Chaochen Zhou, Naijun Zhan, and Bican Xia. Recent advances in pro-gram verification through computer algebra. Frontiers of Computer Science in China,4(1):1-16,2010.
[170]Jingzhong Zhang, Lu Yang, and Xiao-Shan Gao Shang-Ching Chou. Automated production of readable proofs for geometry theorems. Chinese Journal of Com-puters,18:380-393,1995.
[171]Chaochen Zhou. Program verification through computer algebra. In Zhiming Liu and Jifeng He, editors, ICFEM'2006:8th International Conference on Formal En-gineering Methods, volume 4260 of LNCS, page 1, Macao, China,2006. Springer-Berlin.
[172]Richard Zippel. Probabilistic algorithms for sparse polynomials. In Edward W. Ng, editor, EUROSAM'79:International Symposiumon on Symbolic and Alge-braic Computation, volume 72 of LNCS, pages 216-226, Marseille, France,1979. Springer-Berlin.
[2]http://theory.stanford.edu/srirams/Software/sting.html.
[3]http://www-spiral.lip6.fr/wang/epsilon/.
[4]http://www.astree.ens.fr/.
[5]http://www.is.pku.edu.cn/-xbc/software.html.
[6]http://www.maplesoft.com.
[7]http://www.mmrc.iss.ac.cn/mmp/.
[8]http://www.mpi-inf.mpg.de/rybal/rankfinder/.
[9]http://www.risc.uni-linz.ac.at/research/theorema.
[10]http://www.singular.uni-kl.de/.
[11]http://www.wolfram.com/products/mathematica/index.html.
[12]高小山,王定康,裘宗燕,杨宏.方程求解与机器证明.科学出版社,北京,2006.
[13]杨路,张景中,侯晓荣.非线性代数方程组与定理机器证明.上海科技教育出版社,上海,1996.
[14]杨路,候晓荣,曾振柄.多项式的完全判别系统.中国科学(E),26：424-441,1996.
[15]符红光,杨路,曾振柄.构造广义sturm序列的递归算法.中国科学(E),29：546-555,1999.
[16]王东明,杨路,李志斌.符号计算选讲.清华大学出版社,2003.
[17]王东明,夏壁灿,李子明.计算机代数.清华大学出版社,2006.
[18]吴顺堂,邓之光.有限差分方程概论.河海大学出版社,1993.
[19]张景中,梁松新.复系数多项式完全判别系统及其自动生成.中国科学(E),29：61-75，1999.
[20]杨路,夏壁灿.不等式机器证明与自动发现.科学出版社,北京,2008.
[21]吴文俊.复兴构造性的数学.数学进展,(14)：334-339,1985.
[22]张景中.计算机怎样解几何题.暨南大学出版社,广州,2000.
[23]刘木兰.Grobner基理论及其应用.科学出版社,2000.
[24]王东明.消去法及其应用.科学出版社,北京,2002.
[25]李大潜.谈谈现代应用数学.中国科学院院刊,(18)：219-222,2003.
[26]杨德庄.灵活的数学技术.数学进展,(34)：1-16,2005.
[27]陈应华.用实代数方法寻找不变量和秩函数.Master's thesis,北京大学,北京,2007.
[28]毕忠勤.基于实代数符号计算的程序验证技术研究.PhD thesis,华东师范大学,上海,2009.
[29]Building a better bug-trap. Economist Magazine, June 2003.
[30]John Abbott, Anna Maria Bigatti, Martin Kreuzer, and Lorenzo Robbiano. Com-puting ideals of points. Journal of Symbolic Computation,30(4):341-356,2000.
[31]William W. Adams and Philippe Loustaunau. An Introduction to Grobner Bases. American Mathematical Society,1994.
[32]Rajeev Alur and Thomas A. Henzinger. Real-time logics:Complexity and expres-siveness. In LICS'1990:Fifth Annual IEEE Symposium on Logic in Computer Science, pages 390-401, Philadelphia, Pennsylvania, USA,1990. IEEE Computer Society.
[33]Krzysztof R. Apt and Ernst-Rudiger Olderog. Verification of Sequential and Con-current Programs. Springer-Verlag,2nd edition,1997.
[34]Domagoj Babic, Alan J. Hu, Zvonimir Rakamaric, and Byron Cook. Proving termi-nation by divergence. In SEFM'2007:Software Engineering and Formal Methods, pages 93-102, London, England, UK,2007. IEEE COMPUTER SOCIETY.
[35]Josh Berdine, Aziem Chawdhary, Byron Cook, Dino Distefano, and Peter W. O'Hearn. Variance analyses from invariance analyses. In Martin Hofmann and Matthias Felleisen, editors, POPL'2007:Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 211-224, Nice, France,2007. ACM Press.
[36]Josh Berdine, Byron Cook, Dino Distefano, and Peter W. O'Hearn. Automatic termination proofs for programs with shape-shifting heaps. In Thomas Ball and Robert B. Jones, editors, CAV'2006:Computer Aided Verification, volume 4144 of LNCS, pages 386-400, Seattle, WA, USA,2006. Springer-Verlag.
[37]Zhongqin Bi, Meijing Shan, and Bin Wu. Non-termination analysis of linear loop programs with conditionals. In ASEA'2008:Advanced Software Engineering and Its Applications, pages 159-164, Hainan Island, China,2008. IEEE COMPUTER SOCIETY.
[38]Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Linear ranking with reach-ability. In CAV'2005:Computer Aided Verification, volume 3576 of LNCS, pages 491-504, Edinburgh, Scotland, UK,2005. Springer-Verlag.
[39]Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Termination analysis of integer linear loops. In CONCUR'2005:Concurrency Theory,16th International Conference, volume 3653 of LNCS, pages 488-502, San Francisco, CA, USA, 2005. Springer-Verlag.
[40]Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. Termination of polynomial programs. In Radhia Cousot, editor, VMCAI'2005:Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS, pages 113-129, Paris, Frence, 2005. Springer-Verlag.
[41]Mark Braverman. Termination of integer linear programs. In Thomas Ball and Robert B. Jones, editors, CAV'2006:Computer Aided Verification, volume 4144 of LNCS, pages 372-385, Seattle, WA, USA,2006. Springer-Verlag.
[42]Bruno Buchberger. An Algorithm for Finding the Basis Elements in the Residue Class Ring Modulo a Zero Dimensional Polynomial Ideal. PhD thesis, Mathemat-ical Institue, University of Innsbruck, Austria,1965.
[43]Bruno Buchberger. An algorithmical criterion for the solvability of algebraic sys-tems of equations. Aequationes Mathematicae,4(3):374-383,1970.
[44]Bruno Buchberger. Grobner-Bases:An Algorithmic Method in Polynomial Ideal Theory. Reidel Publishing Company, Dodrecht-Boston-Lancaster,1985.
[45]Bruno Buchberger. Practical and theoretical aspects of program verification. In Computer Aided Verification of Information Systems, Romanian-Austrian Work-shop, Timisoara, Romania, February 2003.
[46]Bruno Buchberger and Franz Lichtenberger. Mathematik furInformatiker I:Die Methode der Mathematik. Springer-Verlag, New York,1981.
[47]Tevfik Bultan, Richard Gerber, and William Pugh. Symbolic model checking of infinite state systems using presburger arithmetic. In Orna Grumberg, editor, CAV'1997:Computer Aided Verification, volume 1254 of LNCS, pages 400-411, Haifa, Israel,1997. Springer-Verlag.
[48]Cristiano Calcagno, Dino Distefano, Peter W. O'Hearn, and Hongseok Yang. Foot-print analysis:A shape analysis that discovers preconditions. In Hanne Riis Niel-son and Gilberto File, editors, SAS'2007:Static Analysis,14th International Sym-posium, volume 4634 of LNCS, pages 402-418, Kongens Lyngby, Denmark,2007. Springer-Verlag.
[49]Georg Cantor. Contributions to the Founding of the Theory of Transfinite Num-bers. Dover, New York,1955.
[50]Aziem Chawdhary, Byron Cook, Sumit Gulwani, Mooly Sagiv, and Hongseok Yang. Ranking abstractions. In Sophia Drossopoulou, editor, ESOP'2008:17th European Symposium on Programming, volume 4960 of LNCS, pages 148-162, Budapest, Hungary,2008. Springer-Verlag.
[51]Changbo Chen, Marc Moreno Maza, Bican Xia, and Lu Yang. Computing cylin-drical algebraic decomposition via triangular decomposition. In Jeremy Johnson, Hyungju Park, and Erich Kaltofen, editors, ISSAC'2009:International Sympo-sium on Symbolic and Algebraic Computation, pages 95-102, Seoul, Korea,2009. ACM Press.
[52]Falai Chen, Jiansong Deng, and Yuyu Feng. Algebraic surface blending using wu's method. In Xiao shan Gao and Dongming Wang, editors, ASCM'2000: COMPUTER MATHEMATICS:Proceedings of 4th Asian Symposium on Com-puter Mathematics, volume 8, pages 172-181, Chiang Mai, Thailand,2000. World Scientific.
[53]William Y. C. Chen. A general bijective algorithm for increasing tress. Systems Science and Mathematical Sciences,12:193-203,1999.
[54]Yinghua Chen, Bican Xia, Lu Yang, and Naijun Zhan. Generating polynomial invariants with discoverer and qepcad. In C. B. Jones, Z. Liu, and J. Woodcock, editors, Fonnal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pages 67-82, Macao China. Springer-Verlag.
[55]Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, and Chaochen Zhou. Discov-ering non-linear ranking functions by solving semi-algebraic systems. In Cliff B. Jones, Zhiming Liu, and Jim Woodcock, editors, ICTAC'2007:Theoretical As-pects of Computing, volume 4711 of LNCS, pages 34-49, Macau, China,2007. Springer-Verlag.
[56]George E. Collins. Hauptvortrag:Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, volume 33 of LNCS, pages 134-183, London, UK,1975. Springer-Verlag.
[57]George E. Collins and Hoon Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation,12(3):299-328,1991.
[58]Michael Colon, Sriram Sankaranarayanan, and Henny Sipma. Linear invariant generation using non-linear constraint solving. In Warren A. Hunt Jr. and Fabio Somenzi, editors, CAV'2003:Computer Aided Verification, volume 2725 of LNCS, pages 420-432, Chicago, IL, USA,2003. Springer-Verlag.
[59]Michael Colon and Henny Sipma. Synthesis of linear ranking functions. In Tiziana Margaria and Wang Yi, editors, TACAS'2001, Tools and Algorithms for the Con-struction and Analysis of Systems, volume 2031 of LNCS, pages 67-81, Italy, 2001. Springer-Verlag.
[60]Michael Colon and Henny Sipma. Practical methods for proving program termina-tion. In Ed Brinksma and Kim Guldstrand Larsen, editors, CAV'2002:Computer Aided Verification, volume 2404 of LNCS, pages 442-454, Copenhagen, Den-mark,2002. Springer-Verlag.
[61]Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko, and Moshe Y. Vardi. Proving that programs eventually do something good. In Mar-tin Hofmann and Matthias Felleisen, editors, POPL'2007:Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 265-276, Nice, France,2007. ACM Press.
[62]Byron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, and Mooly Sa-giv. Proving conditional termination. In Aarti Gupta and Sharad Malik, editors, CAV'2008:Computer Aided Verification, volume 5123 of LNCS, pages 328-340, Princeton, NJ, USA,2008. Springer-Verlag.
[63]Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Abstraction refinement for termination. In Chris Hankin and Igor Siveroni, editors, SAS'2005:Static Analysis, volume 3672 of LNCS, pages 87-101, London, UK,2005. Springer-Verlag.
[64]Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Termination proofs for systems code. In Michael I. Schwartzbach and Thomas Ball, editors, PLDI'2006: Conference on Programming Language Design and Implementation, pages 415-426, Ottawa, Ontario, Canada,2006. ACM Press.
[65]Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Terminator:Beyond safety. In Thomas Ball and Robert B. Jones, editors, CAV'2006:Computer Aided Verification, volume 4144 of LNCS, pages 415-418, Seattle, WA, USA,2006. Springer-Verlag.
[66]Byron Cook, Andreas Podelski, and Andrey Rybalchenko. Proving thread termina-tion. In Jeanne Ferrante and Kathryn S. McKinley, editors, PLDI'2007:Proceed-ings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation, pages 320-330, San Diego, California, USA,2007. ACM Press.
[67]Patrick Cousot. Proving program invariance and termination by parametric ab-straction, lagrangian relaxation and semidefinite programming. In Radhia Cousot, editor, VMCAI'2005:Verification, Model Checking, and Abstract Interpretation, volume 3385 of LNCS, pages 1-24, Paris, France,2005. Springer-Verlag.
[68]Patrick Cousot and Radhia Cousot. Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'1977:Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238-252, Los Ange-les, California,1977. ACM Press, New York, NY.
[69]Patrick Cousot and Radhia Cousot. Abstract interpretation and application to logic programs. Journal of Logic Programming,13(2-3):103-179,1992.
[70]Patrick Cousot and Nicolas Halbwachs. Automatic discovery of linear restraints among variables of a program. In POPL'1978:Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 84-96, Tucson, Arizona,1978. ACM Press, New York, NY.
[71]David A. Cox, John B. Little, and Donal O'Shea. Ideals, Varieties, and Algo-rithms:An Introduction to Computational Algebraic Geometry and Commutative Algebra. Springer-Verlag,2005.
[72]David A. Cox, John B. Little, and Donal O'Shea. Using Algebraic Geometry. Springer-Verlag,2nd edition,2005.
[73]Paul Cull, Mary Flahive, and Robby Robson. Difference Equations:From Rabbits to Chaos. Springer,2005.
[74]David Delmas and Jean Souyris. Astree:From research to industry. In Hanne Riis Nielson and Gilberto File, editors, SAS'2007:14th International Symposium on Static Analysis, volume 4634 of LNCS, pages 437-451, Kongens Lyngby,2007. Springer-Berlin.
[75]Edsger W. Dijkstra. Notes on structured programming. In O.-J. Dahl, E. W. Dijk-stra, and C. A. R. Hoare, editors, Structured Programming, London,1972. Aca-demic Press.
[76]Edsger W. Dijkstra. A Discipline of Programming. Prentice-Hall Inc, New Jersey, 1976.
[77]Edsger W. Dijkstra and Carel S. Scholten. Predicate calculus and program seman-tics. Springer-Verlag, New York,1990.
[78]Saber Elaydi. An Introduction to Difference Equations. Springer, New York,3rd edition,2005.
[79]Julius Farkas. Uber die theorie der einfachen ungleichungen. Journal fur die Reine und Angewandte Mathematik,124:1-27.
[80]Robert W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Math-ematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics, pages 19-32, Providence, Rhode Island,1967. American Mathematical Socity.
[81]Ralf Froberg. An Introduction to Grobner Bases. John Wiley & Sons,1998.
[82]Gerald Futschek. Programmentwicklung und Verifikation. Springer-Verlag, Wien, New York,1989.
[83]Steven M. German and Ben Wegbreit. A synthesizer of inductive assertions. IEEE Transactions on Software Engineering,1(1):68-75,1975.
[84]David Gries. The Science of Programming. Springer-Verlag, New York,1981.
[85]Sumit Gulwani, Saurabh Srivastava, and Ramarathnam Venkatesan. Program anal-ysis as constraint solving. In Rajiv Gupta and Saman P. Amarasinghe, editors, PLDI'2008:Proceedings of the ACM SIGPLAN 2008 Conference on Program-ming Language Design and Implementation, volume 43, pages 281-292, Tucson, AZ, USA,2008. ACM.
[86]A. Gupta, T. Henzinger, R. Majumdar, A. Rybalchenko, and R. Xu. Proving non-termination. In George C. Necula and Philip Wadler, editors, POPL'2008:Princi-ples of programming languages, pages 147-158, San Francisco, California, USA, 2008. ACM Press.
[87]Venkatesan Guruswami and Madhu Sudan. Improved decoding of reed-solomon and algebraic-geometry codes. IEEE Transactions on Information Theory, 45(6):1757-1767,1999.
[88]Thomas A. Henzinger and Pei-Hsin Ho. Algorithmic analysis of nonlinear hy-brid systems. In Pierre Wolper, editor, CAV'1995:Computer Aided Verification, volume 939 of LNCS, pages 225-238, Liege, Belgium,1995. Springer-Verlag.
[89]Heisuke Hironaka. The resolution of singularities of an algebraic variety over a field of characteristic zero. Annals of Mathematics,79:109-326,1964.
[90]C. A. R. Hoare. An axiomatic basis for computer programming. Communications of ACM,12(10):576-580, October 1969.
[91]Tony Hoare. The verifying compiler:A grand challenge for computing research. Journal of the ACM,50(1):63-69,2003.
[92]K. Hoffman and R. Kunze. Linear algebra. Prentice-Hall, New Jersey,2n edition, 1971.
[93]Peter Vincent Homeier. Trustworthy Tools for Trustworthy Programs:A Me-chanically Verified Verification Condition Generator for the Total Correctness of Procedures. PhD thesis, Universitiy of California,1995.
[94]Charles Jordan. Calculus of Finite Difference. Chelsea Publishing Company, New York,3rd edition,1965.
[95]Erich Kaltofen and Zhengfeng Yang. On exact and approximate interpolation of sparse rational functions. In Dongming Wang, editor, ISSAC'2007:International Symposium on Symbolic and Algebraic Computation, pages 203-210, Waterloo, Ontario, Canada,2007. ACM Press.
[96]Deepak Kapur. Automatically generating loop invariants using quantifier elimina-tion. In ACA'04:Proc. IMACS Intl. Conf. on Applications of Computer Algebra, Beaumont, Texas,2004.
[97]Deepak Kapur and Joseph L. Mundy. Wu's method and its application to perspec-tive viewing. Artificial Intelligence,37(1-3):15-36,1988.
[98]Michael Karr. Affine relationships among variables of a program. Acta Informat-ica,6:133-151,1976.
[99]Shmuel Katz and Zohar Manna. Logical analysis of programs. Communications of ACM,19(4):188-206,1976.
[100]Manuel Kauers and Burkhard Zimmermann. Computing the algebraic relations of c-finite sequences and multisequences. Journal of Symbolic Computation, 43(11):787-803,2008.
[101]Martin Kirchner. Program verification with the mathematical software system Theorema. PhD thesis, Research Institute for Symbolic Computation, Johannes Kepler University of Linz, Austria,1999.
[102]Ralf Koetter and Alexander Vardy. Algebraic soft-decision decoding of reed-solomon codes. IEEE Transactions on Information Theory,49(11):2809-2825, 2003.
[103]Laura Ildiko Kovacs. Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema. PhD thesis, Research Institute for Symbolic Computation, Johannes Kepler University of Linz, Austria,2007.
[104]Laura Ildiko Kovacs. Reasoning algebraically about p-solvable loops. In C. R. Ramakrishnan and Jakob Rehof, editors, TACAS'2008:Tools and Algorithms for the Construction and Analysis of Systems, volume 4963 of LNCS, pages 249-264, Budapest, Hungary,2008. Springer-Verlag.
[105]Laura Ildiko Kovacs and Tudor Jebelean. Automated generation of loop invariants by recurrence solving in theorema. Annals of the West University of Timisoara. Series Mathematics-Computer Science, XLⅡ:151-166,2004. Special issue on Computer Science-Proceedings of SYNASC'04.
[106]Laura Ildiko Kovacs and Tudor Jebelean. Generation of loop invariants in the-orema by combinatorial and algebraic methods. Bulletins for Applied and Com-puter Mathematics, CVI(2172):125-134,2004. Proceedings of Pannonian Applied Mathematical Meetings, PC-144.
[107]Laura Ildiko Kovacs and Tudor Jebelean. An algorithm for automated generation of invariants for loops with conditionals. In SYNASC'2005:Proceedings of the Seventh International Symposium on Symbolic and Numeric Algorithms for Sci-entific Computing, pages 245-249. IEEE Computer Society,2005.
[108]Laura Ildiko Kovacs and Tudor Jebelean. Finding polynomial invariants for im-perative loops in the theorema system. In Proceeding of Verify 2006 Workshop, pages 52-67,2006.
[109]Gerardo Lafferriere, George J. Pappas, and Shankar Sastry.0-minimal hybrid systems. Mathematics of Control, Signals, and Systems,13:1-21,2000.
[110]Gerardo Lafferriere, George J. Pappas, and Sergio Yovine. Symbolic reachability computation for families of linear vector fields. Journal of Symbolic Computation, 32(3):231-253,2001.
[111]Reinhard Laubenbacher and Brandilyn Stigler. A computational algebra approach to the reverse engineering of gene regulatory networks. Journal of Theoretical Biology,229:523-537,2004.
[112]K. Rustan M. Leino. Efficient weakest preconditions. Information Processing Letters,93(6):281-288,2005.
[113]Stefan Leue and Wei Wei. A region graph based approach to termination proofs. In Holger Hermanns and Jens Palsberg, editors, TACAS'2006:Tools and Algorithms for the Construction and Analysis of Systems, volume 3920 of LNCS, pages 318-333, Vienna, Austria,2006. Springer-Verlag.
[114]Hongbo Li. Clifford algebra approaches to mechanical geometry theorem proving. In Xiao-Shan Gao and Dongming Wang, editors, Mathematics Mechanication, pages 205-229, London, UK,2000. Academic Press.
[115]Stephen Magill, Josh Berdine, Edmund M. Clarke, and Byron Cook. Arithmetic strengthening for shape analysis. In Hanne Riis Nielson and Gilberto File, editors, SAS'2007:Static Analysis,14th International Symposium, volume 4634 of LNCS, pages 419-436, Kongens Lyngby, Denmark,2007. Springer-Verlag.
[116]Zohar Manna and Amir Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York,1995.
[117]M. G. Marinari, H. Michael Moller, and T. Mora. Grobner bases of ideals de-fined by functionals with an application to ideals of projective points. Applicable Algebra in Engineering, Communication and Computing,4(2):103-145,1993.
[118]Richard K. Miller and Anthony N. Michel. Ordinary differential equations. Aca-demic Press, New York,1982.
[119]H. Michael Moller and Bruno Buchberger. The construction of multivariate poly-nomials with preassigned zeros. In Jacques Calmet, editor, EUROCAM'1982:Eu-ropean Computer Algebra Conference, volume 144 of LNCS, pages 24-31, Mar-seille, France,1982. Springer, Berlin-New York.
[120]Markus Muller-Olm, Michael Petter, and Helmut Seidl. Interprocedurally ana-lyzing polynomial identities. In Bruno Durand and Wolfgang Thomas, editors, STACS'2006:23rd Annual Symposium on Theoretical Aspects of Computer Sci-ence, volume 3884 of LNCS, pages 50-67, Marseille, France,2006. Springer-Verlag.
[121]Markus Muller-Olm and Helmut Seidl. Polynomial constants are decidable. In Manuel V. Hermenegildo and German Puebla, editors, SAS'2002:Static Analysis, 9th International Symposium, volume 2477 of LNCS, pages 4-19, Madrid, Spain, 2002. Springer-Verlag.
[122]Markus Muller-Olm and Helmut Seidl. Computing polynomial program invariants. Information Processing Letters,91(5):233-244,2004.
[123]Markus Muller-Olm and Helmut Seidl. A note on karr's algorithm. In Josep Diaz, Juhani Karhumaki, Arto Lepisto, and Donald Sannella, editors, ICALP'2004: 31st International Colloquium on Automata, Languages and Programming, vol-ume 3142 of LNCS, pages 1016-1028, Turku, Finland,2004. Springer-Verlag.
[124]Markus Muller-Olm and Helmut Seidl. Precise interprocedural analysis through linear algebra. In POPL'2004:Proceedings of the 31 st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 330-341, Venice, Italy, 2004. ACM Press, New York, NY.
[125]Michael Petter. Berechnung von polynomiellen invarianten. Master's thesis, Fakultat fur Informatik, Technische Universitat Munchen, Austria,2004.
[126]Giovanni Pistone, Eva Riccomagno, and Henry P. Wynn. Algebraic Statistics: Computational Commutative Algebra in Statistics. Monographs on Statistics & Applied Probability. Chapman & Hall/CRC,2001.
[127]Andreas Podelski and Andrey Rybalchenko. A complete method for the synthe-sis of linear ranking functions. In Bernhard Steffen and Giorgio Levi, editors, VMCAI'2004:Verification, Model Checking, and Abstract Interpretation, volume 2937 of LNCS, pages 239-251, Venice, Italy,2004. Springer-Verlag.
[128]Enric Rodriguez-Carbonell and Deepak Kapur. Automatic generation of polyno-mial loop invariants:Algebraic foundations. In ISSAC'2004:Proceedings of the 2004 international symposium on Symbolic and algebraic computation, pages 266-273, Santander, Spain,2004. ACM Press, New York, NY.
[129]Enric Rodriguez-Carbonell and Deepak Kapur. Generating all polynomial invari-ants in simple loops. Journal of Symbolic Computation,42(4):443-476,2007.
[130]Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Petri net analysis using invariant generation. In Nachum Dershowitz, editor, Verification:Theory and Practice 2003, volume 2772 of LNCS, pages 682-701. Springer-Verlag,2003.
[131]Sriram Sankaranarayanan, Henny Sipma, and Zohar Manna. Constructing in-variants for hybrid systems. In Rajeev Alur and George J. Pappas, editors, HSCC'2004:7th International Workshop on Hybrid Systems:Computation and Control, volume 2993 of LNCS, pages 539-554, Philadelphia, PA, USA,2004. Springer-Verlag.
[132]Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Constraint-based linear-relations analysis. In Roberto Giacobazzi, editor, SAS'2004:11th Inter-national Symposium on Static Analysis, volume 3148 of LNCS, pages 53-68, Verona, Italy,2004. Springer.
[133]Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Non-linear loop invariant generation using grobner bases. In POPL'2004:Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 318-329, Venice, Italy,2004. ACM Press, New York, NY.
[134]Alexander Schrijver. Theory of Linear and Integer Programming. Wiley, John & Sons,1986.
[135]Jacob T. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. Journal of the ACM,27(4):701-717,1980.
[136]Liyong Shen, Min Wu, Zhengfeng Yang, and Zhenbing Zeng. Finding positively invariant sets of a class of nonlinear loops via curve fitting. In SNC'09:Proceed- ings of the 2009 conference on Symbolic numeric computation, pages 185-190, Kyoto, Japan,2009. ACM Press.
[137]D.R. Smart. Fixed Piont Theorems. Cambridge University Press,1980.
[138]Gary Stix. Send in the terminator:A microsoft tool looks for programs that freeze up. Scientific American Magazine, November 2006.
[139]Christopher Strachey. An impossible program. Computer Journal,7(4):313,1965.
[140]Madhu Sudan. Decoding of reed solomon codes beyond the error-correction bound. Journal of Complexity,13(1):180-193,1997.
[141]Ashish Tiwari. Termination of linear programs. In Rajeev Alur and Doron Peled, editors, CAV'2004:Computer Aided Verification, volume 3114 of LNCS, pages 70-82, Boston, MA, USA,2004. Springer-Verlag.
[142]Ashish Tiwari. An algebraic approach for the unsatisfiability of nonlinear con-straints. In C.-H. Luke Ong, editor, CSL'2005:19th International Workshop on Computer Science Logic, volume 3634 of LNCS, pages 248-262, Oxford, UK, 2005. Springer-Berlin.
[143]Ashish Tiwari and Gaurav Khanna. Series of abstractions for hybrid automata. In Claire Tomlin and Mark R. Greenstreet, editors, HSCC'2002:Hybrid Systems: Computation and Control, volume 2289 of LNCS, pages 465-478, Stanford, CA, USA,2002. Springer-Berlin.
[144]Ashish Tiwari, Harald RueB, Hassen Saidi, and Natarajan Shankar. A technique for invariant generation. In Tiziana Margaria and Wang Yi, editors, TACAS'2001: 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, volume 2031 of LNCS, pages 113-127, Genova, Italy,2001. Springer-Verlag.
[145]Alan Turing. On computable numbers, with an application to the entschei-dungsproblem. London Mathematical Socity,42(2):230-265,1936.
[146]Joachim von zur Gathen and Jurgen Gerhard. Modern Computer Algebra. Cam-bridge University Press,2nd edition,2003.
[147]Dongming Wang. Elimination Practice:Software Tools and Applications. Impe-rial College Press, London,2004.
[148]Ben Wegbreit. The synthesis of loop predicates. Communications of ACM, 17(2):102-112,1974.
[149]Ben Wegbreit. Property extraction in well-founded property set. IEEE Transac-tions on Software Engineering, 1(3):270-9285,1975.
[150]Volker Weispfenning. Quantifier elimination for real algebra-the quadratic case and beyond. Applicable Algebra in Engineering, Communication and Computing, 8(2):85-101,1997.
[151]Jinzhao Wu and Zhuojun Liu. Well-behaved inference rules for first-order theorem proving. Journal of Automated Reasoning,21(3):381-400,1998.
[152]Wen-Tsun Wu. A mechanization method of geometry and its applications iv. some theorems in planar kinematics. System Science and Mathematical Scienc, (2):97-109,1989.
[153]Wen-Tsun Wu. On the chemical equlibrium problem and equation-solving. Acta Mathematica Sinica, (10):361-374,1990.
[154]Wen-Tsun Wu. Mechanical theorem proving of differential geometries and some of its applications in mechanics. Journal of Automated Beasoning, (7):171-191, 1991.
[155]Wen-Tsun Wu. Mathematics Mechanization:Mechanical Geometry Theorem-Proving, Mechanical Geometry Problem-Solving, and Polynomial Equations-Solving. Kluwer Academic Publishers, Norwell, MA, USA,2001.
[156]Bican Xia. Discoverer:A tool for solving problems involving polynomial inequal-ities. In et al Yang W-C, editor, ATCM'2000:5th Asian Technology Conference in Mathematics, pages 472-481, Chiang Mai, Thailand,2000.
[157]Bican Xia, Rong Xiao, and Lu Yang. Solving parametric semi-algebraic systems. In Sung il Pae and H. Park, editors, ACSM'2005:7th Asian Symposium on Com-puter Mathematics, pages 153-156, Seoul, Korea,2005.
[158]Bican Xia and Lu Yang. An algorithm for isolating the real solutions of semi-algebraic systems. Journal of Symbolic Computation,34(5):461-477,2002.
[159]Bican Xia, Lu Yang, and Naijun Zhan. Program verification by reduction to semi-algebraic systems solving. In Tiziana Margaria and Bernhard Steffen, editors, ISoLA'2008:Leveraging Applications of Formal Methods, Verification and Val-idation, volume 17 of Communications in Computer and Information Science, pages 277-291, Porto Sani, Greece,2008. Springer-Verlag.
[160]Bican Xia, Lu Yang, Naijun Zhan, and Zhihai Zhang. Symbolic decision procedure for termination of linear programs. to appear in Formal Aspects of Computing.
[161]Lu Yang. Practical automated reasoning on inequalities:Generic programs for inequality proving and discovering. In Wei-Chi Yang, Kiyoshi Shirayanagi, Sung-Chi Chu, and Gary Fitz-Gerald, editors, ATCM'1998:Asian Technology Confer-ence in Mathematics, pages 24-35, Tsukuba, Japan,1998. Springer-Verlag.
[162]Lu Yang. Recent advances in automated theorem proving on inequalities. Journal of Computer Science and Technology,14(5):434-446,1999.
[163]Lu Yang. Recent advances on determining the number of real roots of parametric polynomials. Journal of Symbolic Computation,28(1-2):225-242,1999.
[164]Lu Yang and Bican Xia. Real solution classifications of a class of parametric semi-algebraic systems. In A. Dolzmann, A. Seidl, and T. Sturm, editors, A3L'2005: Algorithmic Algebra and Logic, pages 281-289,2005.
[165]Lu Yang and Shihong Xia. An inequality-proving program applied to global op-timization. In Wei-Chi Yang, Sung-Chi Chu, and Jen-Chung Chuan, editors, ATCM'2000:Asian Technology Conference in Mathematics, pages 40-51, Chi-ang Mai, Thailand,2000.
[166]Lu Yang, Naijun Zhan, Bican Xia, and Chaochen Zhou. Program verification by using discoverer. In Bertrand Meyer and Jim Woodcock, editors, VSTTE'2005: Verified Software:Theories, Tools, Experiments, volume 4171 of LNCS, pages 528-538, Zurich, Switzerland,2005. Springer-Verlag.
[167]Lu Yang and Jingzhong Zhang. A practical program of automated proving for a class of geometric inequalities. In ADG'00:3rd International Workshop on Automated Deduction in Geometry, pages 41-57, London, UK,2000. Springer-Verlag.
[168]Lu Yang, Jingzhong Zhang, and Weinian Zhang. On number of circles intersected by a line. Journal of Combinatorial Theory(Series A),98(2):395-405,2002.
[169]Lu Yang, Chaochen Zhou, Naijun Zhan, and Bican Xia. Recent advances in pro-gram verification through computer algebra. Frontiers of Computer Science in China,4(1):1-16,2010.
[170]Jingzhong Zhang, Lu Yang, and Xiao-Shan Gao Shang-Ching Chou. Automated production of readable proofs for geometry theorems. Chinese Journal of Com-puters,18:380-393,1995.
[171]Chaochen Zhou. Program verification through computer algebra. In Zhiming Liu and Jifeng He, editors, ICFEM'2006:8th International Conference on Formal En-gineering Methods, volume 4260 of LNCS, page 1, Macao, China,2006. Springer-Berlin.
[172]Richard Zippel. Probabilistic algorithms for sparse polynomials. In Edward W. Ng, editor, EUROSAM'79:International Symposiumon on Symbolic and Alge-braic Computation, volume 72 of LNCS, pages 216-226, Marseille, France,1979. Springer-Berlin.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |