程序验证与系统分析中的若干符号计算问题
|
摘要
形式化方法是开发高可信软件和安全攸关系统的有效途径,是高可信计算的研究重点之一。高可信计算追求软件和系统提供可信赖的计算服务能力,而这种可信赖性是建立在严格数学证明上的。形式化方法主要研究软硬件系统的规格描述、开发过程、以及检测验证,特别是程序正确性证明和系统安全性分析。研究的问题有活性、安全性、公平性、终止性、不变式、同步、异步、互斥、可达性、持续性、稳定性等。
在处理这些程序和系统中的分析与验证问题时,传统的逻辑方法会因为状态空间爆炸而无法检测出全部错误,不能彻底地保证安全性；单纯数值计算又会产生浮点误差,影响整体的可靠性。因而,近年来研究者正在尝试使用以绝对准确性为目标的符号计算方法来处理它们,即将这些性质的检验问题转换成代数系统的求解问题。特别是随着计算机性能和计算机数学的不断发展,为开展该方向的研究提供了强有力的支撑。
本文的主要贡献由以下几部分组成：
1.理论部分：主要研究了若干种广义多项式的实根隔离问题。在M. Achatz等人2008年的工作基础上,提出了用连分数技巧逼近超越数ex和区间算术思想进行准确计算,改进了现有指数多项式实根隔离算法；同时对于幂指数多项式,推广了伪导数序列的构造方法,证明了广义Budan-Fourier定理对其仍然成立,并给出一个正根隔离近似算法。
2.应用部分：主要尝试了将上述理论成果应用在程序验证和系统分析领域。方面,利用估计多指数多项式实根界算法,完善了A.Tiwari在2004年关于线性循环终止性的结论。在其终止性可判定理论的基础上,对于给定非终止循环构造出其非终止输入作为反例,使该结果更加完整。另一方面,将广义多项式实根隔离算法用于判定线性系统的可达性问题,除去了线性系统矩阵的可对角化限制,丰富了输入函数的类型,扩展了G.Lafferrierre等人在2001年的结果。
3.软件部分：主要在计算机代数系统MAPLE下编制了程序包REACH,能够准确求解任意由指数多项式等式和不等式所组成系统,实现了判定有理特征值线性系统可达性的数学机械化,能集成在一般混成系统的验证工具中。
Formal method is an effective approach to develop trustworthy softwares and safety-critical systems. It is also one of the most important topics in trustworthy computing. Trustworthy computing pursues the reliable computing services, whom need to be proved by rigorously mathematical reasoning. Formal method stares at the specification, develop-ment, checking and verification of software and hardware systems, specially for proving the correctness of programs and analyzing the safety of systems. Their core tasks include liveness, safety, fairness, termination, invariant, synchronization, asynchronization, ex-clusion, reachability, duration, stability and so on.
For the problems in program verification and system analysis, the traditional logic method can not determine the whole safety since it would suffer from the state space ex-plosion and fail to find out all bugs. And purely numerical computation would involve floating-point errors, thus affects the reliability in large. So recent research resorts to symbolic computation, which places excessive emphasis on the absolute exactness, that is, reducing the problem of checking safety properties to that of solving algebraic systems. More importantly, this method is quite feasible and promising owing to the increasing-powerful computer performance and the growing-mature computer mathematics.
The main contributions of this thesis are as follows:
1. Theory:The real root isolation problems in several generalized polynomials are well studied. Based on M. Achatz's work (2008), we present a tip of continued fraction for approaching to the transcendent number ex and compute the exact value with interval arithmetic, thus improve the existing algorithm for isolating the real roots of exponential polynomials. In the meanwhile, we also develop the construc-tion of pseudo-derivative sequences for power-exponential polynomials, prove the generalized Budan-Fourier theorem for them, and give an algorithm for isolating their positive roots approximately.
2. Application:We dedicate the above theoretic results to the fields of program ver-ification and system analysis. On one hand, we present an algorithm for estimat-ing the real root bounds of multi-exponential polynomials, to supplement the re-sult about the termination of linear loops in A. Tiwari's work (2004). Under his termination-deciding method, a nonterminating input can be further constructed as an counterexample for the given nonterminating loop, which makes the result more complete. On the other hand, we successfully decide the reachability of linear sys-tems by the algorithms of isolating those generalized polynomials'real roots. We remove the restriction that the matrices of linear systems must be diagonalizable and enlarge the scope of input functions, thus enrich G. Lafferrierre's work (2001).
3. Software:Based on the computer algebra system MAPLE, we provide a program package REACH, which can exactly solve the arbitrary system consisting of expo-nential polynomial equations and inequalities. It implements mathematics mecha-nization of deciding the reachability of rational eigenvalue linear systems, and can be integrated into verification tools for general hybrid systems.
在处理这些程序和系统中的分析与验证问题时,传统的逻辑方法会因为状态空间爆炸而无法检测出全部错误,不能彻底地保证安全性；单纯数值计算又会产生浮点误差,影响整体的可靠性。因而,近年来研究者正在尝试使用以绝对准确性为目标的符号计算方法来处理它们,即将这些性质的检验问题转换成代数系统的求解问题。特别是随着计算机性能和计算机数学的不断发展,为开展该方向的研究提供了强有力的支撑。
本文的主要贡献由以下几部分组成：
1.理论部分：主要研究了若干种广义多项式的实根隔离问题。在M. Achatz等人2008年的工作基础上,提出了用连分数技巧逼近超越数ex和区间算术思想进行准确计算,改进了现有指数多项式实根隔离算法；同时对于幂指数多项式,推广了伪导数序列的构造方法,证明了广义Budan-Fourier定理对其仍然成立,并给出一个正根隔离近似算法。
2.应用部分：主要尝试了将上述理论成果应用在程序验证和系统分析领域。方面,利用估计多指数多项式实根界算法,完善了A.Tiwari在2004年关于线性循环终止性的结论。在其终止性可判定理论的基础上,对于给定非终止循环构造出其非终止输入作为反例,使该结果更加完整。另一方面,将广义多项式实根隔离算法用于判定线性系统的可达性问题,除去了线性系统矩阵的可对角化限制,丰富了输入函数的类型,扩展了G.Lafferrierre等人在2001年的结果。
3.软件部分：主要在计算机代数系统MAPLE下编制了程序包REACH,能够准确求解任意由指数多项式等式和不等式所组成系统,实现了判定有理特征值线性系统可达性的数学机械化,能集成在一般混成系统的验证工具中。
Formal method is an effective approach to develop trustworthy softwares and safety-critical systems. It is also one of the most important topics in trustworthy computing. Trustworthy computing pursues the reliable computing services, whom need to be proved by rigorously mathematical reasoning. Formal method stares at the specification, develop-ment, checking and verification of software and hardware systems, specially for proving the correctness of programs and analyzing the safety of systems. Their core tasks include liveness, safety, fairness, termination, invariant, synchronization, asynchronization, ex-clusion, reachability, duration, stability and so on.
For the problems in program verification and system analysis, the traditional logic method can not determine the whole safety since it would suffer from the state space ex-plosion and fail to find out all bugs. And purely numerical computation would involve floating-point errors, thus affects the reliability in large. So recent research resorts to symbolic computation, which places excessive emphasis on the absolute exactness, that is, reducing the problem of checking safety properties to that of solving algebraic systems. More importantly, this method is quite feasible and promising owing to the increasing-powerful computer performance and the growing-mature computer mathematics.
The main contributions of this thesis are as follows:
1. Theory:The real root isolation problems in several generalized polynomials are well studied. Based on M. Achatz's work (2008), we present a tip of continued fraction for approaching to the transcendent number ex and compute the exact value with interval arithmetic, thus improve the existing algorithm for isolating the real roots of exponential polynomials. In the meanwhile, we also develop the construc-tion of pseudo-derivative sequences for power-exponential polynomials, prove the generalized Budan-Fourier theorem for them, and give an algorithm for isolating their positive roots approximately.
2. Application:We dedicate the above theoretic results to the fields of program ver-ification and system analysis. On one hand, we present an algorithm for estimat-ing the real root bounds of multi-exponential polynomials, to supplement the re-sult about the termination of linear loops in A. Tiwari's work (2004). Under his termination-deciding method, a nonterminating input can be further constructed as an counterexample for the given nonterminating loop, which makes the result more complete. On the other hand, we successfully decide the reachability of linear sys-tems by the algorithms of isolating those generalized polynomials'real roots. We remove the restriction that the matrices of linear systems must be diagonalizable and enlarge the scope of input functions, thus enrich G. Lafferrierre's work (2001).
3. Software:Based on the computer algebra system MAPLE, we provide a program package REACH, which can exactly solve the arbitrary system consisting of expo-nential polynomial equations and inequalities. It implements mathematics mecha-nization of deciding the reachability of rational eigenvalue linear systems, and can be integrated into verification tools for general hybrid systems.
引文
[1]A. van der Schaft, H. Schumacher, An Introduction to Hybrid Dynamical Systems, Springer, Berlin,2000,[中译本：宋永华等译,“混成动态系统引论”,清华大学出版社,北京,2007].
[2]H. H. Goldstine, J. von Neumann, Planning and coding problems for an electronic computer instrument, in:A. H. Traub (Ed.), Collected Works of John von Neu-mann, Vol.5, Pergamon Press, New York,1963, pp.80-235.
[3]R. W. Floyd, Assigning meanings to programs, in:J. T. Schwartz (Ed.), Mathemat-ical Aspects of Computer Science, American Mathematical Society, Providence, RI, US,1967, pp.19-32.
[4]E. W. Dijkstra, A constructive approach to the problem of program correctness, BIT Numerical Mathematics 8 (3) (1968) 174-186.
[5]C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM 12 (10) (1969) 576-580.
[6]P. Cousot, R. Cousot, Abstract interpretation:A unified lattice model for static anal-ysis of programs by construction or approximation of fixpoints, in:POPL 1977, ACM Press, New York,1977, pp.238-252.
[7]P. Cousot, Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming, in:R. Cousot (Ed.), VMCAI 2005, LNCS 3385, Springer, Berlin,2005, pp.1-24.
[8]B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Mon-niaux, X. Rival, Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, in:T. (?). Mogensen, D. A. Schmidt, I. H. Sudborough (Eds.), The Essence of Computation:Complexity, Analysis, Transformation, LNCS 2566, Springer, Berlin,2002, pp.85-108. [9] E. A. Emerson, E. M. Clarke, Characterizing correctness properties of parallel pro-grams using fixpoints, in:J. W. de Bakker, J. van Leeuwen (Eds.), ICALP 1980, LNCS 85, Springer, Berlin,1980, pp.169-181.
[10]P. E. Allen, S. Bose, E. M. Clarke, S. Michaylov, PARTHENON:A parallel the-orem prover for non-horn clauses, in:E. L. Lusk, R. A. Overbeek (Eds.), CADE 1988, LNCS 310, Springer, Berlin,1988, pp.764-765.
[11]J. P. Queille, J. Sifakis, Specification and verification of concurrent systems in CE-SAR, in:M. Dezani-Ciancaglini, U. Montanari (Eds.), Symposium on Program-ming 1982, LNCS 137, Springer, Berlin,1982, pp.337-351.
[12]Z. Manna, A. Pnueli, Verifying hybrid systems, in:R. L. Grossman, A. Nerode, A. P. Ravn, H. Rischel (Eds.), Hybrid Systems, LNCS 736, Springer, Berlin,1993, pp.4-35.
[13]N. Bjorner, A. Browne, E. Y. Chang, M. A. Colon, A. Kapur, Z. Manna, H. B. Sipma, T. E. Uribe, STeP:Deductive-algorithmic verification of reactive and real-time systems, in:R. Alur, T. A. Henzinger (Eds.), CAV 1996, LNCS 1102, Springer, Berlin,1996, pp.415-418.
[14]R. Alur, D. L. Dill, The theory of timed automata, in:J. W. de Bakker, C. Huizing, W. R. de Roever, G. Rozenberg (Eds.), REX Workshop 1991, LNCS 600, Springer, Berlin,1992, pp.45-73."
[15]A. Puri, P. Varaiya, Decidability of hybrid systems with rectangular differential inclusions, in:D. L. Dill (Ed.), CAV 1994, LNCS 818, Springer, Berlin,1994, pp. 95-104.
[16]T. A. Henzinger, P. W. Kopke, A. Puri, P. Varaiya, What's decidable about hybrid automata?, Journal of Computer and System Sciences 57 (1) (1998) 94-124.
[17]E. Asarin, O. Maler, A. Pnueli, Reachability analysis of dynamical systems having piecewise-constant derivatives, Theoretical Computer Science 138 (1) (1995) 35-65.
[18]B. Cook, A. Podelski, A. Rybalchenko, TERMINATOR:Beyond safety, in:T. Ball, R. B. Jones (Eds.), CAV 2006, LNCS 4144, Springer, Berlin,2006, pp.415-418.
[19]M. L. Bujorianu, J. Lygeros, Toward a general theory of stochastic hybrid systems, in:H. A. P. Blom, J. Lygeros (Eds.), Stochastic Hybrid Systems, Lecture Notes in Control and Information Sciences, Springer, Berlin,2006, pp.3-30.
[20]F. D. Torrisi, A. Bemporad, HYSDEL—a tool for generating computational hybrid models for analysis and synthesis problems, IEEE Transactions on Control Systems Technology 12 (2) (2004) 235-249.
[21]A. Lecchini-Visintini, W. Glover, J. Lygeros, J. M. Maciejowski, Monte carlo opti-mization for conflict resolution in air traffic control, IEEE Transactions on Intelli-gent Transportation Systems 7 (4) (2006) 470-482.
[22]A. Platzer, E. M. Clarke, Computing differential invariants of hybrid systems as fixedpoints, in:A. Gupta, S. Malik (Eds.), CAV 2008, LNCS 5123, Springer, Berlin,2008, pp.176-189.
[23]A. Platzer, J.-D. Quesel, KeYmaera:A hybrid theorem prover for hybrid systems, in:A. Armando, P. Baumgartner, G. Dowek (Eds.), IJCAR 2008, LNCS 5195, Springer, Berlin,2008, pp.171-178.
[24]C. C. Zhou, C. A. R. Hoare, A. Ravn, A calculus of durations, Information Pro-cessing Letters 40 (5) (1991) 269-276.
[25]H. M. Lin, PAM:A process algebra manipulator, Formal Methods in System De-sign 7(3)(1995) 243-259.
[26]W. Li, S. M. Luan, Operational and complete approaches to belief revision, Journal of Computer Science and Technology 15 (3) (2000) 202-212.
[27]J. Wang, H. W. Chen, Temporal reasoning about real time reactive systems, in:Z. S. Shi (Ed.), IWAR 1992, IFIP Transactions, North-Holland, Amsterdam,1992, pp.249-256.
[28]C. A. R. Hoare, J. F. He, Unifying Theories of Programming, Series in Computer Science, Prentice Hall, New Jersey,1998.
[29]S. C. Johnson, Tricks for improving Kronecker's method, Bell Laboratories Report.
[30]B. Buchberger, An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal, Phd thesis, University of Innsbruck, Austria (1965).
[31]G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, in:H. Brakhage (Ed.), Automata Theory and Formal Languages 1975, LNCS 33, Springer, Berlin,1975, pp.134-183.
[32]G. E. Collins, H. Hong, Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation 12 (3) (1991) 299-328.
[33]吴文俊,数学机械化,数学机械化丛书,科学出版社,北京,2003.
[34]吴文俊,几何定理机器证明的基本原理(初等几何部分),计算机科学丛书,科学出版社,北京,1984.
[35]杨路,侯晓荣,曾振柄,多项式的完全判别系统,中国科学E辑26(5)(1996)424-441.
[36]张景中,梁松新,复系数多项式完全判别系统及其自动生成,中国科学E辑29(1)(1999)61-75.
[37]杨路,张景中,侯晓荣,非线性代数方程组与定理机器证明,非线性科学丛书,上海科技教育出版社,上海,1996.
[38]杨路,夏壁灿,不等式机器证明与自动发现,数学机械化丛书,科学出版社,北京,2008.
[39]A. R. Bradley, Z. Manna, Verification constraint problems with strengthening, in: K. Barkaoui, A. Cavalcanti, A. Cerone (Eds.), ICTAC 2006, LNCS 4281, Springer, Berlin,2006, pp.35-49.
[40]Y. H. Chen, B. C. Xia, L. Yang, N. J. Zhan, C. C. Zhou, Discovering non-linear ranking functions by solving semi-algebraic systems, in:C. B. Jones, Z. M. Liu, J. Woodcock (Eds.), ICTAC 2007, LNCS 4711, Springer, Berlin,2007, pp.34-49.
[41]M. A. Colon, H. B. Sipma, Practical methods for proving program termination, in: E. Brinksma, K. G. Larsen (Eds.), CAV 2002, LNCS 2404, Springer, Berlin,2002, pp.442-454.
[42]D. Kapur, A quantifier-elimination based heuristic for automatically generating in-ductive assertions for programs, Journal of Systems Science and Complexity 19 (3) (2006)307-330.
[43]B. C. Xia, L. Yang, N. J. Zhan, Program verification by reduction to semi-algebraic systems solving, in:T. Margaria, B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation, Communications in Computer and Information Science, Springer, Berlin,2008, pp.277-291.
[44]L. Yang, N. J. Zhan, B. C. Xia, C. C. Zhou, Program verification by using DISCOV-ERER, in:B. Meyer, J. Woodcock (Eds.), VSTTE 2005, LNCS 4171, Springer, Berlin,2005, pp.528-538.
[45]E. Rodriguez-Carbonell, D. Kapur, Generating all polynomial invariants in simple loops, Journal of Symbolic Computation 42 (4) (2007) 443-476.
[46]S. Sankaranarayanan, H. B. Sipma, Z. Manna, Non-linear loop invariant generation using Grobner bases, in:POPL 2004, ACM Press, New York,2004, pp.318-329.
[47]S. Sankaranarayanan, H. B. Sipma, Z. Manna, Constructing invariants for hybrid systems, in:R. Alur, G. J. Pappas (Eds.), HSCC 2004, LNCS 2993, Springer, Berlin,2004, pp.539-554.
[48]N. Popov, Functional program verification in Theorema, Phd thesis, RISC, Jo-hannes Kepler University, Linz, Austria (2008).
[49]H. Anai, V. Weispfenning, Reach set computations using real quantifier elimina-tion, in:M. D. D. Benedetto, A. L. Sangiovanni-Vincentelli (Eds.), HSCC 2001, LNCS 2034, Springer, Berlin,2001, pp.63-76.
[50]G. Lafferriere, G. J. Pappas, S. Yovine, Symbolic reachability computaion for fam-ilies of linear vector fields, Journal of Symbolic Computation 32 (3) (2001) 231-253.
[51]S. Ratschan, Z. K. She, Safety verification of hybrid systems by constraint propa-gation based abstraction refinement, in:M. Morari, L. Thiele (Eds.), HSCC 2005, LNCS 3414, Springer, Berlin,2005, pp.573-589.
[52]M. Achatz, S. McCallum, V. Weispfenning, Deciding polynomial-exponential problems, in:ISSAC 2008, ACM Press, New York,2008, pp.215-222.
[53]A. Strzebonski, Real root isolation for exp-log functions, in:ISSAC 2008, ACM Press, New York,2008, pp.303-313.
[54]M. Xu, L. Y. Chen, Z. B. Zeng, Z. B. Li, Reachability analysis of rational eigen-value linear systems, International Journal of Systems Science, accepted.
[55]M. Xu, C. D. Mu, Z. B. Zeng, Z. B. Li, A heuristic approach to positive root isolation for multiple power sums, Journal of Universal Computer Science, revised.
[56]M. Xu, L. Y. Chen, Z. B. Zeng, Z. B. Li, Real root isolation of multi-exponential polynomials with application, in:M. S. Rahman, S. Fujita (Eds.), WALCOM 2010, LNCS 5942, Springer, Berlin,2010, pp.263-268.
[57]E. Artin, Galois Theory:Lectures Delivered at the University of Notre Dame,2nd Edition, University of Notre Dame Press, Notre Dame,1944,[中译本：李同孚译,“伽罗华理论”,上海科学技术出版社,上海,1979].
[58]D. S. Bridges, Computability:A Mathematical Sketchbook, GTM 246, Springer, Berlin,1994.
[59]甘特马赫尔(著),柯召(译),矩阵论(上下卷),高等教育出版社,北京,1955.
[60]D. E. Knuth, Art of Computer Programming, Vol.2:Seminumerical Algorithms, 3rd Edition, Addison-Wesley, New York,1997,[中译本：苏运霖译,“计算机程序设计艺术(第2卷)：半数值算法”,国防工业出版社,北京,2002].
[61]A. G. Akritas, Vincent's theorem in algebraic manipulation, Phd thesis, North Car-olina State University, Raleigh, NC, US (1978).
[62]G. E. Collins, R. Loos, Real zeros of polynomials, in:B. Buchberger, G. E. Collins, R. Loos (Eds.), Computer Algebra:Symbolic and Algebraic Computation,2nd Edition, Springer, Berlin,1983, pp.83-94.
[63]J. V. Uspensky, Theory of Equations, McGraw-Hill, New York,1948.
[64]G. E. Collins, E. Horowitz, The minimum root separation of a polynomial, Mathe-matics of Computation 28 (1974) 589-597.
[65]A. G. Akritas, Linear and quadratic complexity bounds on the values of the positive roots of polynomials, Journal of Universal Computer Science 15 (3) (2009) 523-537.
[66]F. Rouillier, P. Zimmermann, Efficient isolation of polynomial's real roots, Journal of Computational and Applied Mathematics 162 (1) (2004) 33-50.
[67]L. Yang, Recent advances on determining the number of real roots of parametric polynomials, Journal of Symbolic Computation 28 (1-2) (1999) 225-242.
[68]D. Marker, Model Theory:An Introduction, GTM 217, Springer, Berlin,2002.
[69]王世强,模型论基础,现代数学基础丛书23,科学出版社,北京,1987.
[70]A. Tarski, A Decision Method for Elementary Algebra and Geometry,2nd Edition, University of California Press, Berkeley,1951,[中译本：陆钟万译,“初等代数和几何的判定法”,科学出版社,北京,1959].
[71]L. van den Dries, Remarks on Tarski's problem concerning (R,+,·,exp), in:G. Lolli, G. Longo, A. Marcja (Eds.), Logic Colloquium 1982, Elsevier, Amsterdam, 1982, pp.97-121.
[72]N. Jacobson, Basic Algebra I, W. H. Freeman and Company, San Francisco,1974,[中译本：上海师范大学数学系代数教研室译,“基础代数”,高等教育出版社,北京,1988].
[73]H. Cohen, A Course in Computational Algebraic Number Theory, GTM 138, Springer, Berlin,1996.
[74]C. L. Siegel, Transcendental Numbers, Princeton University Press, New Jersey, 1949,[中译本：魏道政译,“超越数”,科学出版社,北京,1958].
[75]冯贝叶,多项式和无理数,哈尔滨工业大学出版社,哈尔滨,2008.
[76]C. D. Olds, Continued Fractions, New Mathmatical Library 9, Random House, New York,1963,[中译本：张顺燕译,“连分数”,北京大学出版社,北京,1985].
[77]A. G. Akritas, Elements of Computer Algebra with Applications, Wiley, New York, 1989.
[78]R. L. Graham, D. E. Knuth, O. Patashnik, Concrete Mathematics:A Foundation for Computer Science,2nd Edition, Addison-Wesley, New York,1994,[中译本：庄心谷译,“具体数学”,西安电子科技大学出版社,西安,1992].
[79]G. Polya, G. Szego, Problems and Theorems in Analysis, Vol.2:Theory of Func-tions. Zeros. Polynomials. Determinants. Number Theory. Geometry, Classics in Mathematics, Springer, Berlin,1976,[中译本：张奠宙等译,“数学分析中的问题 与定理(第2卷)：函数论.零点.多项式.行列式.数论.几何”,上海科学技术出版社,上海,1985].
[80]M. Mignotte, Some useful bounds, in:B. Buchberger, G. E. Collins, R. Loos (Eds.), Computer Algebra:Symbolic and Algebraic Computation,2nd Edition, Springer, Berlin,1983, pp.259-263.
[81]王东明(Ed.),符号计算选讲,清华大学出版社,北京,2003.
[82]D. Stefanescu, New bounds for positive roots of polynomials, Journal of Universal Computer Science 11 (12) (2005) 2125-2131.
[83]G. H. Hardy, E. M. Wright, An Introduction to The Theory of Numbers,5th Edi-tion, Oxford University Press, Oxford,1979,[中译本：张明尧等译,“数论导引”,人民邮电出版社,北京,2008].
[84]Z. Manna, Mathematical Theory of Computation, McGraw-Hill, New York,1974,[中译本：李玉茜等译,“计算的数学理论”,科学出版社,北京,1986].
[85]A. Tiwari, Termination of linear programs, in:R. Alur, D. A. Peled (Eds.), CAV 2004, LNCS 3114, Springer, Berlin,2004, pp.70-82.
[86]M. Xu, L. Y. Chen, Z. B. Zeng, Z. B. Li, Termination analysis of linear loops, International Journal of Foundations of Computer Science, accepted.
[87]H. K. Berg, W. E. Boebrt, W. R. Franta, T. G. Moher, Formal Methods of Program Verification and Specification, Series in Software, Prentice Hall, New Jersey,1982,[中译本：宋国新等译,“程序验证和规范的形式方法”,科学出版社,北京,1988].
[88]O.-J. Dahl, E. W. Dijkstra, C. A. R. Hoare, Structured Programming, Studies in Data Processing 8, Academic Press, New York,1972,[中译本：陈火旺等译,“结构程序设计”,科学出版社,北京,1980].
[89]M. D. Davis, E. J. Weyuker, Computability, Complexity, and Languages:Funda-mentals of Theoretical Computer Science, Academic Press, New York,1983, [中译本：张立昂等译,“可计算性,复杂性,语言：理论计算机科学基础”,清华大学出版社,北京,1989].
[90]B. C. Xia, Z. H. Zhang, Termination of linear programs with nonlinear constraints, available at http://arxiv.org/abs/0904.3588vl.
[91]Y. Matiyasevich, Hilbert's Tenth Problem, MIT Press, London,1993.
[92]A. R. Bradley, Z. Manna, H. B. Sipma, Termination of polynomial programs, in: R. Cousot (Ed.), VMCAI 2005, LNCS 3385, Springer, Berlin,2005, pp.113-129.
[93]A. R. Bradley, Z. Manna, H. B. Sipma, The polyranking principle, in:L. Caires, G. F. Italiano, L. Monteiro, C. Palamidessi, M. Yung (Eds.), ICALP 2005, LNCS 3580, Springer, Berlin,2005, pp.1349-1361.
[94]S. Leue, W. Wei, A region graph based approach to termination proofs, in:H. Hermanns, J. Palsberg (Eds.), TACAS 2006, LNCS 3920, Springer, Berlin,2006, pp.318-333.
[95]A. Podelski, A. Rybalchenko, Transition invariants, in:LICS 2004, IEEE Com-puter Society,2004, pp.32-41.
[96]A. Podelski, A. Rybalchenko, Transition predicate abstraction and fair termination, ACM Transactions on Programming Languages and Systems 29 (3) (2007) 132-144.
[97]F. P. Ramsey, On a problem of formal logic, Proceedings of the London Mathemat-ical 30 (1930) 264-286.
[98]M. Xu, Z. B. Li, Termination of programs in nested loops, 计算机科学35 (10A) (2008)167-169.
[99]R. K. Guy, Unsolved Problems in Number Theory,2nd Edition, Problem Books in Mathematics, Springer, Berlin,1994,[中译本：张明尧译,“数论中未解决的问题”,科学出版社,北京,2003].
[100]B. C. Xia, L. Yang, N. J. Zhan, Z. H. Zhang, Symbolic decision procedure for termination of linear programs, Formal Aspects of Computing, accepted.
[101]M. Braverman, Termination of integer linear programs, in:T. Ball, R. B. Jones (Eds.), CAV 2006, LNCS 4144, Springer, Berlin,2006, pp.372-385.
[102]B. Mishra, Algorithmic Algebra, Texts and Monographs in Computer Science, Springer, Berlin,1993.
[103]A. R. Bradley, Z. Manna, H. B. Sipma, What's decidable about arrays?, in:E. A. Emerson, K. S. Namjoshi (Eds.), VMCAI 2006, LNCS 3855, Springer, Berlin, 2006, pp.427-442.
[104]A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, R.-G. Xu, Proving non-termination, in:POPL 2008, ACM Press, New York,2008, pp.147-158.
[105]K. Hoffman, R. Kunze, Linear Algebra,2nd Edition, Prentice Hall, New Jersey, 1971.
[106]V. I. Istratescu, Fixed Point Theory:An Introduction, Mathematics and Its Appli-cations 7, Springer, Berlin,2001.
[107]T. Kailath, Linear Systems, Prentice Hall, New Jersey,1980,[中译本：李清泉等译,“线性系统”,科学出版社,北京,1985].
[108]Y. Hakan, G. J. Pappas, Geometric programming relaxations for linear system reachability, in:Proceedings of American Control Conference,2004, pp.553-559.
[109]O. Karabacak, N. S. Sengor, A dwell time approach to the stability of switched linear systems based on the distance between eigenvector sets, International Journal of Systems Science 40 (8) (2009) 845-853.
[110]C. A. Desoer, J. Wing, A minimal time discrete system, IRE Transactions on Au-tomatic Control 6 (2)(1961) 111-125.
[111]P. Collins, Continuity and computability of reachable sets, Theoretical Computer Science 341(1) (2005) 162-195.
[112]T. Dang, O. Maler, Reachability analysis via face lifting, in:T. A. Henzinger, S. Sastry (Eds.), HSCC 1998, LNCS 1386, Springer, Berlin,1998, pp.96-109.
[113]S. V. Rakovic, E. C. Kerrigan, D. Q. Mayne, J. Lygeros, Reachability analysis of discrete-time systems with disturbances, IEEE Transactions on Automatic Control 51 (4) (2006) 546-561.
[114]A. B. Kurzhanski, P. Varaiya, Ellipsoidal techniques for reachability analysis, in: N. A. Lynch, B. H. Krogh (Eds.), HSCC 2000, LNCS 1790, Springer, Berlin,2000, pp.202-214.
[115]I. Mitchell, C. Tomlin, Level set method for computation in hybrid systems, in:N. A. Lynch, B. H. Krogh (Eds.), HSCC 2000, LNCS 1790, Springer, Berlin,2000, pp.310-323.
[116]A. Platzer, Differential dynamic logic for hybrid systems, Journal of Automated Reasoning 41 (2) (2008) 143-189.
[117]A. Platzer, Differential-algebraic dynamic logic for differential-algebraic pro-grams, Journal of Logic and Computation 20 (1) (2010) 309-352.
[118]A. Tiwari, G. Khanna, Nonlinear systems:Approximating reach sets, in:R. Alur, G. J. Pappas (Eds.), HSCC 2004, LNCS 2993, Springer, Berlin,2004, pp.600-614.
[119]X. M. Zhang, M. M. Li, M. Wu, J. H. She, Further results on stability and stabilisa-tion of linear systems with state and input delays, International Journal of Systems Science 40 (1) (2009) 1-10.
[120]G. Lafferriere, G. J. Pappas, S. Sastry,0-minimal hybrid systems, Mathematics of Control, Signals, and Systems 13 (1) (2000) 1-21.
[121]M. Xu, L. Y. Chen, Z. B. Li, Symbolic reachability computation of a class of non-linear systems, in:ICIS 2009, IEEE Computer Society,2009, pp.706-710.
[122]M. Xu, L. Y. Chen, Z. B. Li, Symbolic reachability computation of a class of second-order systems, in:ICIA 2009, IEEE Computer Society,2009, pp.1336-1339.
[123]E. Kamke, Differentialgleichungen, B. G. Teubner GmbH, Leipzig,1967,[中译本：张鸿林译,“常微分方程手册”,科学出版社,北京,1977].
[124]A. Nerode, R. A.Shore, Logic for Applications,3rd Edition, Graduate Texts in Computer Science, Springer, Berlin,1997,[中译本：丁德成等译,“应用逻辑”,机械工业出版社,北京,2007].
[125]N. Wirth, Algorithms+Data Structures=Programs, Series in Automatic Com-putation, Prentice Hall, New Jersey,1976,[中译本：曹德和等译,“算法+数据结构=程序”,科学出版社,北京,1984].
[126]R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, Cam-bridge,1985,[中译本：杨奇译,“矩阵分析”,机械工业出版社,北京,2005].
[2]H. H. Goldstine, J. von Neumann, Planning and coding problems for an electronic computer instrument, in:A. H. Traub (Ed.), Collected Works of John von Neu-mann, Vol.5, Pergamon Press, New York,1963, pp.80-235.
[3]R. W. Floyd, Assigning meanings to programs, in:J. T. Schwartz (Ed.), Mathemat-ical Aspects of Computer Science, American Mathematical Society, Providence, RI, US,1967, pp.19-32.
[4]E. W. Dijkstra, A constructive approach to the problem of program correctness, BIT Numerical Mathematics 8 (3) (1968) 174-186.
[5]C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM 12 (10) (1969) 576-580.
[6]P. Cousot, R. Cousot, Abstract interpretation:A unified lattice model for static anal-ysis of programs by construction or approximation of fixpoints, in:POPL 1977, ACM Press, New York,1977, pp.238-252.
[7]P. Cousot, Proving program invariance and termination by parametric abstraction, lagrangian relaxation and semidefinite programming, in:R. Cousot (Ed.), VMCAI 2005, LNCS 3385, Springer, Berlin,2005, pp.1-24.
[8]B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Mon-niaux, X. Rival, Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, in:T. (?). Mogensen, D. A. Schmidt, I. H. Sudborough (Eds.), The Essence of Computation:Complexity, Analysis, Transformation, LNCS 2566, Springer, Berlin,2002, pp.85-108. [9] E. A. Emerson, E. M. Clarke, Characterizing correctness properties of parallel pro-grams using fixpoints, in:J. W. de Bakker, J. van Leeuwen (Eds.), ICALP 1980, LNCS 85, Springer, Berlin,1980, pp.169-181.
[10]P. E. Allen, S. Bose, E. M. Clarke, S. Michaylov, PARTHENON:A parallel the-orem prover for non-horn clauses, in:E. L. Lusk, R. A. Overbeek (Eds.), CADE 1988, LNCS 310, Springer, Berlin,1988, pp.764-765.
[11]J. P. Queille, J. Sifakis, Specification and verification of concurrent systems in CE-SAR, in:M. Dezani-Ciancaglini, U. Montanari (Eds.), Symposium on Program-ming 1982, LNCS 137, Springer, Berlin,1982, pp.337-351.
[12]Z. Manna, A. Pnueli, Verifying hybrid systems, in:R. L. Grossman, A. Nerode, A. P. Ravn, H. Rischel (Eds.), Hybrid Systems, LNCS 736, Springer, Berlin,1993, pp.4-35.
[13]N. Bjorner, A. Browne, E. Y. Chang, M. A. Colon, A. Kapur, Z. Manna, H. B. Sipma, T. E. Uribe, STeP:Deductive-algorithmic verification of reactive and real-time systems, in:R. Alur, T. A. Henzinger (Eds.), CAV 1996, LNCS 1102, Springer, Berlin,1996, pp.415-418.
[14]R. Alur, D. L. Dill, The theory of timed automata, in:J. W. de Bakker, C. Huizing, W. R. de Roever, G. Rozenberg (Eds.), REX Workshop 1991, LNCS 600, Springer, Berlin,1992, pp.45-73."
[15]A. Puri, P. Varaiya, Decidability of hybrid systems with rectangular differential inclusions, in:D. L. Dill (Ed.), CAV 1994, LNCS 818, Springer, Berlin,1994, pp. 95-104.
[16]T. A. Henzinger, P. W. Kopke, A. Puri, P. Varaiya, What's decidable about hybrid automata?, Journal of Computer and System Sciences 57 (1) (1998) 94-124.
[17]E. Asarin, O. Maler, A. Pnueli, Reachability analysis of dynamical systems having piecewise-constant derivatives, Theoretical Computer Science 138 (1) (1995) 35-65.
[18]B. Cook, A. Podelski, A. Rybalchenko, TERMINATOR:Beyond safety, in:T. Ball, R. B. Jones (Eds.), CAV 2006, LNCS 4144, Springer, Berlin,2006, pp.415-418.
[19]M. L. Bujorianu, J. Lygeros, Toward a general theory of stochastic hybrid systems, in:H. A. P. Blom, J. Lygeros (Eds.), Stochastic Hybrid Systems, Lecture Notes in Control and Information Sciences, Springer, Berlin,2006, pp.3-30.
[20]F. D. Torrisi, A. Bemporad, HYSDEL—a tool for generating computational hybrid models for analysis and synthesis problems, IEEE Transactions on Control Systems Technology 12 (2) (2004) 235-249.
[21]A. Lecchini-Visintini, W. Glover, J. Lygeros, J. M. Maciejowski, Monte carlo opti-mization for conflict resolution in air traffic control, IEEE Transactions on Intelli-gent Transportation Systems 7 (4) (2006) 470-482.
[22]A. Platzer, E. M. Clarke, Computing differential invariants of hybrid systems as fixedpoints, in:A. Gupta, S. Malik (Eds.), CAV 2008, LNCS 5123, Springer, Berlin,2008, pp.176-189.
[23]A. Platzer, J.-D. Quesel, KeYmaera:A hybrid theorem prover for hybrid systems, in:A. Armando, P. Baumgartner, G. Dowek (Eds.), IJCAR 2008, LNCS 5195, Springer, Berlin,2008, pp.171-178.
[24]C. C. Zhou, C. A. R. Hoare, A. Ravn, A calculus of durations, Information Pro-cessing Letters 40 (5) (1991) 269-276.
[25]H. M. Lin, PAM:A process algebra manipulator, Formal Methods in System De-sign 7(3)(1995) 243-259.
[26]W. Li, S. M. Luan, Operational and complete approaches to belief revision, Journal of Computer Science and Technology 15 (3) (2000) 202-212.
[27]J. Wang, H. W. Chen, Temporal reasoning about real time reactive systems, in:Z. S. Shi (Ed.), IWAR 1992, IFIP Transactions, North-Holland, Amsterdam,1992, pp.249-256.
[28]C. A. R. Hoare, J. F. He, Unifying Theories of Programming, Series in Computer Science, Prentice Hall, New Jersey,1998.
[29]S. C. Johnson, Tricks for improving Kronecker's method, Bell Laboratories Report.
[30]B. Buchberger, An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal, Phd thesis, University of Innsbruck, Austria (1965).
[31]G. E. Collins, Quantifier elimination for real closed fields by cylindrical algebraic decomposition, in:H. Brakhage (Ed.), Automata Theory and Formal Languages 1975, LNCS 33, Springer, Berlin,1975, pp.134-183.
[32]G. E. Collins, H. Hong, Partial cylindrical algebraic decomposition for quantifier elimination, Journal of Symbolic Computation 12 (3) (1991) 299-328.
[33]吴文俊,数学机械化,数学机械化丛书,科学出版社,北京,2003.
[34]吴文俊,几何定理机器证明的基本原理(初等几何部分),计算机科学丛书,科学出版社,北京,1984.
[35]杨路,侯晓荣,曾振柄,多项式的完全判别系统,中国科学E辑26(5)(1996)424-441.
[36]张景中,梁松新,复系数多项式完全判别系统及其自动生成,中国科学E辑29(1)(1999)61-75.
[37]杨路,张景中,侯晓荣,非线性代数方程组与定理机器证明,非线性科学丛书,上海科技教育出版社,上海,1996.
[38]杨路,夏壁灿,不等式机器证明与自动发现,数学机械化丛书,科学出版社,北京,2008.
[39]A. R. Bradley, Z. Manna, Verification constraint problems with strengthening, in: K. Barkaoui, A. Cavalcanti, A. Cerone (Eds.), ICTAC 2006, LNCS 4281, Springer, Berlin,2006, pp.35-49.
[40]Y. H. Chen, B. C. Xia, L. Yang, N. J. Zhan, C. C. Zhou, Discovering non-linear ranking functions by solving semi-algebraic systems, in:C. B. Jones, Z. M. Liu, J. Woodcock (Eds.), ICTAC 2007, LNCS 4711, Springer, Berlin,2007, pp.34-49.
[41]M. A. Colon, H. B. Sipma, Practical methods for proving program termination, in: E. Brinksma, K. G. Larsen (Eds.), CAV 2002, LNCS 2404, Springer, Berlin,2002, pp.442-454.
[42]D. Kapur, A quantifier-elimination based heuristic for automatically generating in-ductive assertions for programs, Journal of Systems Science and Complexity 19 (3) (2006)307-330.
[43]B. C. Xia, L. Yang, N. J. Zhan, Program verification by reduction to semi-algebraic systems solving, in:T. Margaria, B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation, Communications in Computer and Information Science, Springer, Berlin,2008, pp.277-291.
[44]L. Yang, N. J. Zhan, B. C. Xia, C. C. Zhou, Program verification by using DISCOV-ERER, in:B. Meyer, J. Woodcock (Eds.), VSTTE 2005, LNCS 4171, Springer, Berlin,2005, pp.528-538.
[45]E. Rodriguez-Carbonell, D. Kapur, Generating all polynomial invariants in simple loops, Journal of Symbolic Computation 42 (4) (2007) 443-476.
[46]S. Sankaranarayanan, H. B. Sipma, Z. Manna, Non-linear loop invariant generation using Grobner bases, in:POPL 2004, ACM Press, New York,2004, pp.318-329.
[47]S. Sankaranarayanan, H. B. Sipma, Z. Manna, Constructing invariants for hybrid systems, in:R. Alur, G. J. Pappas (Eds.), HSCC 2004, LNCS 2993, Springer, Berlin,2004, pp.539-554.
[48]N. Popov, Functional program verification in Theorema, Phd thesis, RISC, Jo-hannes Kepler University, Linz, Austria (2008).
[49]H. Anai, V. Weispfenning, Reach set computations using real quantifier elimina-tion, in:M. D. D. Benedetto, A. L. Sangiovanni-Vincentelli (Eds.), HSCC 2001, LNCS 2034, Springer, Berlin,2001, pp.63-76.
[50]G. Lafferriere, G. J. Pappas, S. Yovine, Symbolic reachability computaion for fam-ilies of linear vector fields, Journal of Symbolic Computation 32 (3) (2001) 231-253.
[51]S. Ratschan, Z. K. She, Safety verification of hybrid systems by constraint propa-gation based abstraction refinement, in:M. Morari, L. Thiele (Eds.), HSCC 2005, LNCS 3414, Springer, Berlin,2005, pp.573-589.
[52]M. Achatz, S. McCallum, V. Weispfenning, Deciding polynomial-exponential problems, in:ISSAC 2008, ACM Press, New York,2008, pp.215-222.
[53]A. Strzebonski, Real root isolation for exp-log functions, in:ISSAC 2008, ACM Press, New York,2008, pp.303-313.
[54]M. Xu, L. Y. Chen, Z. B. Zeng, Z. B. Li, Reachability analysis of rational eigen-value linear systems, International Journal of Systems Science, accepted.
[55]M. Xu, C. D. Mu, Z. B. Zeng, Z. B. Li, A heuristic approach to positive root isolation for multiple power sums, Journal of Universal Computer Science, revised.
[56]M. Xu, L. Y. Chen, Z. B. Zeng, Z. B. Li, Real root isolation of multi-exponential polynomials with application, in:M. S. Rahman, S. Fujita (Eds.), WALCOM 2010, LNCS 5942, Springer, Berlin,2010, pp.263-268.
[57]E. Artin, Galois Theory:Lectures Delivered at the University of Notre Dame,2nd Edition, University of Notre Dame Press, Notre Dame,1944,[中译本：李同孚译,“伽罗华理论”,上海科学技术出版社,上海,1979].
[58]D. S. Bridges, Computability:A Mathematical Sketchbook, GTM 246, Springer, Berlin,1994.
[59]甘特马赫尔(著),柯召(译),矩阵论(上下卷),高等教育出版社,北京,1955.
[60]D. E. Knuth, Art of Computer Programming, Vol.2:Seminumerical Algorithms, 3rd Edition, Addison-Wesley, New York,1997,[中译本：苏运霖译,“计算机程序设计艺术(第2卷)：半数值算法”,国防工业出版社,北京,2002].
[61]A. G. Akritas, Vincent's theorem in algebraic manipulation, Phd thesis, North Car-olina State University, Raleigh, NC, US (1978).
[62]G. E. Collins, R. Loos, Real zeros of polynomials, in:B. Buchberger, G. E. Collins, R. Loos (Eds.), Computer Algebra:Symbolic and Algebraic Computation,2nd Edition, Springer, Berlin,1983, pp.83-94.
[63]J. V. Uspensky, Theory of Equations, McGraw-Hill, New York,1948.
[64]G. E. Collins, E. Horowitz, The minimum root separation of a polynomial, Mathe-matics of Computation 28 (1974) 589-597.
[65]A. G. Akritas, Linear and quadratic complexity bounds on the values of the positive roots of polynomials, Journal of Universal Computer Science 15 (3) (2009) 523-537.
[66]F. Rouillier, P. Zimmermann, Efficient isolation of polynomial's real roots, Journal of Computational and Applied Mathematics 162 (1) (2004) 33-50.
[67]L. Yang, Recent advances on determining the number of real roots of parametric polynomials, Journal of Symbolic Computation 28 (1-2) (1999) 225-242.
[68]D. Marker, Model Theory:An Introduction, GTM 217, Springer, Berlin,2002.
[69]王世强,模型论基础,现代数学基础丛书23,科学出版社,北京,1987.
[70]A. Tarski, A Decision Method for Elementary Algebra and Geometry,2nd Edition, University of California Press, Berkeley,1951,[中译本：陆钟万译,“初等代数和几何的判定法”,科学出版社,北京,1959].
[71]L. van den Dries, Remarks on Tarski's problem concerning (R,+,·,exp), in:G. Lolli, G. Longo, A. Marcja (Eds.), Logic Colloquium 1982, Elsevier, Amsterdam, 1982, pp.97-121.
[72]N. Jacobson, Basic Algebra I, W. H. Freeman and Company, San Francisco,1974,[中译本：上海师范大学数学系代数教研室译,“基础代数”,高等教育出版社,北京,1988].
[73]H. Cohen, A Course in Computational Algebraic Number Theory, GTM 138, Springer, Berlin,1996.
[74]C. L. Siegel, Transcendental Numbers, Princeton University Press, New Jersey, 1949,[中译本：魏道政译,“超越数”,科学出版社,北京,1958].
[75]冯贝叶,多项式和无理数,哈尔滨工业大学出版社,哈尔滨,2008.
[76]C. D. Olds, Continued Fractions, New Mathmatical Library 9, Random House, New York,1963,[中译本：张顺燕译,“连分数”,北京大学出版社,北京,1985].
[77]A. G. Akritas, Elements of Computer Algebra with Applications, Wiley, New York, 1989.
[78]R. L. Graham, D. E. Knuth, O. Patashnik, Concrete Mathematics:A Foundation for Computer Science,2nd Edition, Addison-Wesley, New York,1994,[中译本：庄心谷译,“具体数学”,西安电子科技大学出版社,西安,1992].
[79]G. Polya, G. Szego, Problems and Theorems in Analysis, Vol.2:Theory of Func-tions. Zeros. Polynomials. Determinants. Number Theory. Geometry, Classics in Mathematics, Springer, Berlin,1976,[中译本：张奠宙等译,“数学分析中的问题 与定理(第2卷)：函数论.零点.多项式.行列式.数论.几何”,上海科学技术出版社,上海,1985].
[80]M. Mignotte, Some useful bounds, in:B. Buchberger, G. E. Collins, R. Loos (Eds.), Computer Algebra:Symbolic and Algebraic Computation,2nd Edition, Springer, Berlin,1983, pp.259-263.
[81]王东明(Ed.),符号计算选讲,清华大学出版社,北京,2003.
[82]D. Stefanescu, New bounds for positive roots of polynomials, Journal of Universal Computer Science 11 (12) (2005) 2125-2131.
[83]G. H. Hardy, E. M. Wright, An Introduction to The Theory of Numbers,5th Edi-tion, Oxford University Press, Oxford,1979,[中译本：张明尧等译,“数论导引”,人民邮电出版社,北京,2008].
[84]Z. Manna, Mathematical Theory of Computation, McGraw-Hill, New York,1974,[中译本：李玉茜等译,“计算的数学理论”,科学出版社,北京,1986].
[85]A. Tiwari, Termination of linear programs, in:R. Alur, D. A. Peled (Eds.), CAV 2004, LNCS 3114, Springer, Berlin,2004, pp.70-82.
[86]M. Xu, L. Y. Chen, Z. B. Zeng, Z. B. Li, Termination analysis of linear loops, International Journal of Foundations of Computer Science, accepted.
[87]H. K. Berg, W. E. Boebrt, W. R. Franta, T. G. Moher, Formal Methods of Program Verification and Specification, Series in Software, Prentice Hall, New Jersey,1982,[中译本：宋国新等译,“程序验证和规范的形式方法”,科学出版社,北京,1988].
[88]O.-J. Dahl, E. W. Dijkstra, C. A. R. Hoare, Structured Programming, Studies in Data Processing 8, Academic Press, New York,1972,[中译本：陈火旺等译,“结构程序设计”,科学出版社,北京,1980].
[89]M. D. Davis, E. J. Weyuker, Computability, Complexity, and Languages:Funda-mentals of Theoretical Computer Science, Academic Press, New York,1983, [中译本：张立昂等译,“可计算性,复杂性,语言：理论计算机科学基础”,清华大学出版社,北京,1989].
[90]B. C. Xia, Z. H. Zhang, Termination of linear programs with nonlinear constraints, available at http://arxiv.org/abs/0904.3588vl.
[91]Y. Matiyasevich, Hilbert's Tenth Problem, MIT Press, London,1993.
[92]A. R. Bradley, Z. Manna, H. B. Sipma, Termination of polynomial programs, in: R. Cousot (Ed.), VMCAI 2005, LNCS 3385, Springer, Berlin,2005, pp.113-129.
[93]A. R. Bradley, Z. Manna, H. B. Sipma, The polyranking principle, in:L. Caires, G. F. Italiano, L. Monteiro, C. Palamidessi, M. Yung (Eds.), ICALP 2005, LNCS 3580, Springer, Berlin,2005, pp.1349-1361.
[94]S. Leue, W. Wei, A region graph based approach to termination proofs, in:H. Hermanns, J. Palsberg (Eds.), TACAS 2006, LNCS 3920, Springer, Berlin,2006, pp.318-333.
[95]A. Podelski, A. Rybalchenko, Transition invariants, in:LICS 2004, IEEE Com-puter Society,2004, pp.32-41.
[96]A. Podelski, A. Rybalchenko, Transition predicate abstraction and fair termination, ACM Transactions on Programming Languages and Systems 29 (3) (2007) 132-144.
[97]F. P. Ramsey, On a problem of formal logic, Proceedings of the London Mathemat-ical 30 (1930) 264-286.
[98]M. Xu, Z. B. Li, Termination of programs in nested loops, 计算机科学35 (10A) (2008)167-169.
[99]R. K. Guy, Unsolved Problems in Number Theory,2nd Edition, Problem Books in Mathematics, Springer, Berlin,1994,[中译本：张明尧译,“数论中未解决的问题”,科学出版社,北京,2003].
[100]B. C. Xia, L. Yang, N. J. Zhan, Z. H. Zhang, Symbolic decision procedure for termination of linear programs, Formal Aspects of Computing, accepted.
[101]M. Braverman, Termination of integer linear programs, in:T. Ball, R. B. Jones (Eds.), CAV 2006, LNCS 4144, Springer, Berlin,2006, pp.372-385.
[102]B. Mishra, Algorithmic Algebra, Texts and Monographs in Computer Science, Springer, Berlin,1993.
[103]A. R. Bradley, Z. Manna, H. B. Sipma, What's decidable about arrays?, in:E. A. Emerson, K. S. Namjoshi (Eds.), VMCAI 2006, LNCS 3855, Springer, Berlin, 2006, pp.427-442.
[104]A. Gupta, T. A. Henzinger, R. Majumdar, A. Rybalchenko, R.-G. Xu, Proving non-termination, in:POPL 2008, ACM Press, New York,2008, pp.147-158.
[105]K. Hoffman, R. Kunze, Linear Algebra,2nd Edition, Prentice Hall, New Jersey, 1971.
[106]V. I. Istratescu, Fixed Point Theory:An Introduction, Mathematics and Its Appli-cations 7, Springer, Berlin,2001.
[107]T. Kailath, Linear Systems, Prentice Hall, New Jersey,1980,[中译本：李清泉等译,“线性系统”,科学出版社,北京,1985].
[108]Y. Hakan, G. J. Pappas, Geometric programming relaxations for linear system reachability, in:Proceedings of American Control Conference,2004, pp.553-559.
[109]O. Karabacak, N. S. Sengor, A dwell time approach to the stability of switched linear systems based on the distance between eigenvector sets, International Journal of Systems Science 40 (8) (2009) 845-853.
[110]C. A. Desoer, J. Wing, A minimal time discrete system, IRE Transactions on Au-tomatic Control 6 (2)(1961) 111-125.
[111]P. Collins, Continuity and computability of reachable sets, Theoretical Computer Science 341(1) (2005) 162-195.
[112]T. Dang, O. Maler, Reachability analysis via face lifting, in:T. A. Henzinger, S. Sastry (Eds.), HSCC 1998, LNCS 1386, Springer, Berlin,1998, pp.96-109.
[113]S. V. Rakovic, E. C. Kerrigan, D. Q. Mayne, J. Lygeros, Reachability analysis of discrete-time systems with disturbances, IEEE Transactions on Automatic Control 51 (4) (2006) 546-561.
[114]A. B. Kurzhanski, P. Varaiya, Ellipsoidal techniques for reachability analysis, in: N. A. Lynch, B. H. Krogh (Eds.), HSCC 2000, LNCS 1790, Springer, Berlin,2000, pp.202-214.
[115]I. Mitchell, C. Tomlin, Level set method for computation in hybrid systems, in:N. A. Lynch, B. H. Krogh (Eds.), HSCC 2000, LNCS 1790, Springer, Berlin,2000, pp.310-323.
[116]A. Platzer, Differential dynamic logic for hybrid systems, Journal of Automated Reasoning 41 (2) (2008) 143-189.
[117]A. Platzer, Differential-algebraic dynamic logic for differential-algebraic pro-grams, Journal of Logic and Computation 20 (1) (2010) 309-352.
[118]A. Tiwari, G. Khanna, Nonlinear systems:Approximating reach sets, in:R. Alur, G. J. Pappas (Eds.), HSCC 2004, LNCS 2993, Springer, Berlin,2004, pp.600-614.
[119]X. M. Zhang, M. M. Li, M. Wu, J. H. She, Further results on stability and stabilisa-tion of linear systems with state and input delays, International Journal of Systems Science 40 (1) (2009) 1-10.
[120]G. Lafferriere, G. J. Pappas, S. Sastry,0-minimal hybrid systems, Mathematics of Control, Signals, and Systems 13 (1) (2000) 1-21.
[121]M. Xu, L. Y. Chen, Z. B. Li, Symbolic reachability computation of a class of non-linear systems, in:ICIS 2009, IEEE Computer Society,2009, pp.706-710.
[122]M. Xu, L. Y. Chen, Z. B. Li, Symbolic reachability computation of a class of second-order systems, in:ICIA 2009, IEEE Computer Society,2009, pp.1336-1339.
[123]E. Kamke, Differentialgleichungen, B. G. Teubner GmbH, Leipzig,1967,[中译本：张鸿林译,“常微分方程手册”,科学出版社,北京,1977].
[124]A. Nerode, R. A.Shore, Logic for Applications,3rd Edition, Graduate Texts in Computer Science, Springer, Berlin,1997,[中译本：丁德成等译,“应用逻辑”,机械工业出版社,北京,2007].
[125]N. Wirth, Algorithms+Data Structures=Programs, Series in Automatic Com-putation, Prentice Hall, New Jersey,1976,[中译本：曹德和等译,“算法+数据结构=程序”,科学出版社,北京,1984].
[126]R. A. Horn, C. R. Johnson, Matrix Analysis, Cambridge University Press, Cam-bridge,1985,[中译本：杨奇译,“矩阵分析”,机械工业出版社,北京,2005].