基于区间线性抽象域的可靠浮点及非凸静态分析
|
摘要
软件的可信性已成为现代软件质量问题的焦点。发现并排除软件缺陷是构建可信软件的重要途径，这对于航天、国防、汽车等安全攸关应用尤其重要。科学与工程应用相关程序，特别是一些安全攸关嵌入式软件，一般与数学和物理有着紧密的联系，从而不可避免地会包含大量数值计算。因此，许多程序缺陷往往和程序中的数值性质密切相关，比如除零错、算术溢出、数组越界等运行时错误。
抽象解释是一种对程序语义进行近似(或抽象)的通用理论，并为静态分析提供了一个通用的框架。而抽象域则是抽象解释框架下的核心要素，通过选择特定的语义表示和操作算法来发现所关注的性质。数值抽象域可用来自动发现程序中的数值性质，即程序变量间的数值关系。经过数十年的发展，在基于抽象解释的数值程序分析领域，出现了许多面向不同数值性质、表达能力多样的数值抽象域。然而，大部分已有数值抽象域(尤其是关系型抽象域)都是采用多精度有理数来实现以保证可靠性，时空开销较大，从而影响到分析的计算效率和可扩展性；而且，大部分已有数值抽象域在表达能力方面存在凸性局限性，对析取的处理能力较弱；此外，已有数值抽象域尚不支持实际程序分析中常出现的区间系数。
本文主要研究数值抽象域的设计和实现。研究目标包括：探索数值抽象域的可靠浮点构造方法，以通过浮点实现来提高计算效率；设计新的数值抽象域使其能够表达非凸性质并支持区间系数，以通过增强表达能力来提高分析精度。本文主要工作如下：
1)提出了浮点多面体抽象域，作为经典凸多面体域的一种可靠浮点构造方法。凸多面体域是目前表达能力最强、应用最广泛的数值抽象域之一，但是其基于多精度有理数的实现在可扩展性和易处理性方面受到限制。本文仅基于凸多面体的约束表示(无需生成子表示)并采用浮点系数，给出了凸多面体抽象域的一种可靠浮点实现方法，以通过浮点实现来提高凸多面体域的计算效率和处理能力。由于基于约束的多面体域的复杂度主要源于其高代价的接合操作(即凸闭包)，本文还提出了一系列低代价的弱接合操作。
2)把区间线性代数引入到程序分析中，提出了一系列支持区间系数的区间线性抽象域。区间(算术)为构造可靠的浮点抽象域提供了一种自然且有效的途径，并且在实现浮点多面体域过程中也产生了凸多面体表达能力之外的区间线性约束。本文提出了区间多面体抽象域，用以推导程序中变量间的区间线性不等式关系。该域可以看作是经典凸多面体域的区间系数扩展版本。作为一种受限情形，本文还提出了行阶梯形区间线性等式抽象域，用以推导区间线性等式关系。其表示方法基于区间线性等式系统的行阶梯形式，使得该域具有多项式的时空复杂度。该域可以看作是经典仿射等式抽象域的区间系数扩展版本。通过采用区间线性系统的弱解语义，这些区间线性抽象域能够天然地表达某类拓扑非凸(甚至非连通)性质。本文采用浮点数并基于向外舍入的区间算术可靠地实现了这些抽象域。
3)提出了一系列可表达非凸性质的线性绝对值抽象域。绝对值是数学中的一个基本概念，常用来描述数学或物理模型中的分段线性特征，并且可以表达非凸性质。本文给出并证明了线性绝对值不等式系统、区间线性不等式系统、广义线性互补问题(系统)三者之间的等价性，以及线性绝对值等式系统、水平线性互补问题(系统)两者之间的等价性。基于凸多面体的双重描述法，给出了广义线性互补问题(系统)的双重描述法，并作为其应用还给出了一种求解绝对值线性规划问题的新方法。在此基础上，本文提出了线性绝对值不等式抽象域(用来推导线性绝对值不等式／区间线性不等式／广义线性互补不等式关系)和线性绝对值等式抽象域(用来推导线性绝对值等式／水平线性互补等式关系)。线性绝对值不等式域是经典多面体域的一般化，虽然表达能力与区间多面体域相同，但是其域操作都是具体域上对应操作的最佳抽象。而线性绝对值等式域是经典仿射等式域的一般化。基于广义线性互补系统的双重描述法并采用多精度有理数实现了这两个抽象域。
本文提出的数值抽象域在分析精度和计算效率间进行了不同的权衡，可以面向不同的应用。这些抽象域都在数值抽象域库APRON中得以实现，并且实验结果令人鼓舞。
Trustworthiness of software has become the center of attention when consider-ing modern software quality. Finding bugs before release is fundamental to buildtrustworthy software, which is extremely important for safety-critical applicationssuch as aerospace, defense and automotive. Scienti?c and engineering programs es-pecially safety-critical embedded software are usually related to mathematics andphysics, and thus often involve a lot of numerical computations. Hence, many pro-gram bugs including division by zero, arithmetic over?ows and array out-of-bounds,are closely related to numerical properties in the program.
Abstract interpretation is a theory of semantics approximation, allowing thedesign of sound and e?cient static analyses. Abstract domains are a key ingredi-ent in this framework: They enable semantic choices (what properties to infer) andalgorithmic choices (how to compute). In this thesis, we focus on design and im-plementation of numerical abstract domains that are used to automatically discovernumerical properties over program variables. Over the past decades, a wide variety ofnumerical abstract domains have been proposed. However, most existing abstractdomains (especially relational ones) need arbitrary precision rational numbers tobuild implementations, which may degrade the time and memory e?ciency. Mostof them can only represent convex properties, and hence have limitations in deal-ing with disjunctions. Besides, currently there is no abstract domain that supportsinterval variable coe?cients which appear naturally in real-life program analysis.
The goal of this thesis is to explore more e?cient numerical abstract domains,using sound ?oating-point constructions, and to design more precise ones, allowingnon-convex properties and interval coe?cients.
Major contributions of this thesis are listed as follows.
1) We present a so-called ?oating-point polyhedra abstract domain. The clas-sical convex polyhedra domain is one of the most powerful and commonly used ab-stract domains in the ?eld, but rational implementations may su?er from scalabilityproblems. To solve this issue, we present an implementation using ?oating-pointarithmetic without sacri?cing soundness, based on a constraint-only representation using ?oating-point coe?cients. Since its complexity mainly comes from the costlyjoin operation (i.e., polyhedral convex hull), a series of cheap weak join operationsare then proposed.
2) We introduce interval linear algebra to static analysis and propose intervallinear abstract domains that support interval coe?cients. Intervals are naturallysuited to construct sound ?oating-point abstract domains. First, a so-called intervalpolyhedra domain is proposed to infer interval linear inequalities. Then, a restrictedabstract domain is proposed based on a system of interval linear equalities in rowechelon form, polynomial in time and memory. The two domains can be consid-ered as interval extensions of the existing convex polyhedra domain and the a?neequality domain respectively. By interpreting solutions as weak solutions of intervallinear systems, both domains can express certain non-convex (even unconnected)properties. They are soundly implemented using ?oating-point numbers based oninterval arithmetic with outward rounding.
3) We present linear absolute value abstract domains that natively allow toexpress non-convex properties. Absolute value (AV) is fundamental in mathematicsand often used to describe piecewise linear behavior. The equivalence among linearAV inequality systems, interval linear inequality systems and extended linear com-plementarity problem (XLCP) systems is stated. We construct a double descriptionmethod for XLCP on top of that for polyhedra, based on which a new method forsolving AV linear programming problems is shown. On this basis, we propose anabstract domain of linear AV equalities, and an abstract domain of linear AV in-equalities that has the same expressiveness as interval polyhedra domain but enjoysoptimal transfer functions. They are implemented using rational numbers based onthe double description method for XLCP.
The numerical abstract domains presented in this thesis provide di?erent trade-o?s between precision and e?ciency, and can be applied to di?erent problems. Theyare implemented in the APRON library, and experimental results are encouraging.
抽象解释是一种对程序语义进行近似(或抽象)的通用理论，并为静态分析提供了一个通用的框架。而抽象域则是抽象解释框架下的核心要素，通过选择特定的语义表示和操作算法来发现所关注的性质。数值抽象域可用来自动发现程序中的数值性质，即程序变量间的数值关系。经过数十年的发展，在基于抽象解释的数值程序分析领域，出现了许多面向不同数值性质、表达能力多样的数值抽象域。然而，大部分已有数值抽象域(尤其是关系型抽象域)都是采用多精度有理数来实现以保证可靠性，时空开销较大，从而影响到分析的计算效率和可扩展性；而且，大部分已有数值抽象域在表达能力方面存在凸性局限性，对析取的处理能力较弱；此外，已有数值抽象域尚不支持实际程序分析中常出现的区间系数。
本文主要研究数值抽象域的设计和实现。研究目标包括：探索数值抽象域的可靠浮点构造方法，以通过浮点实现来提高计算效率；设计新的数值抽象域使其能够表达非凸性质并支持区间系数，以通过增强表达能力来提高分析精度。本文主要工作如下：
1)提出了浮点多面体抽象域，作为经典凸多面体域的一种可靠浮点构造方法。凸多面体域是目前表达能力最强、应用最广泛的数值抽象域之一，但是其基于多精度有理数的实现在可扩展性和易处理性方面受到限制。本文仅基于凸多面体的约束表示(无需生成子表示)并采用浮点系数，给出了凸多面体抽象域的一种可靠浮点实现方法，以通过浮点实现来提高凸多面体域的计算效率和处理能力。由于基于约束的多面体域的复杂度主要源于其高代价的接合操作(即凸闭包)，本文还提出了一系列低代价的弱接合操作。
2)把区间线性代数引入到程序分析中，提出了一系列支持区间系数的区间线性抽象域。区间(算术)为构造可靠的浮点抽象域提供了一种自然且有效的途径，并且在实现浮点多面体域过程中也产生了凸多面体表达能力之外的区间线性约束。本文提出了区间多面体抽象域，用以推导程序中变量间的区间线性不等式关系。该域可以看作是经典凸多面体域的区间系数扩展版本。作为一种受限情形，本文还提出了行阶梯形区间线性等式抽象域，用以推导区间线性等式关系。其表示方法基于区间线性等式系统的行阶梯形式，使得该域具有多项式的时空复杂度。该域可以看作是经典仿射等式抽象域的区间系数扩展版本。通过采用区间线性系统的弱解语义，这些区间线性抽象域能够天然地表达某类拓扑非凸(甚至非连通)性质。本文采用浮点数并基于向外舍入的区间算术可靠地实现了这些抽象域。
3)提出了一系列可表达非凸性质的线性绝对值抽象域。绝对值是数学中的一个基本概念，常用来描述数学或物理模型中的分段线性特征，并且可以表达非凸性质。本文给出并证明了线性绝对值不等式系统、区间线性不等式系统、广义线性互补问题(系统)三者之间的等价性，以及线性绝对值等式系统、水平线性互补问题(系统)两者之间的等价性。基于凸多面体的双重描述法，给出了广义线性互补问题(系统)的双重描述法，并作为其应用还给出了一种求解绝对值线性规划问题的新方法。在此基础上，本文提出了线性绝对值不等式抽象域(用来推导线性绝对值不等式／区间线性不等式／广义线性互补不等式关系)和线性绝对值等式抽象域(用来推导线性绝对值等式／水平线性互补等式关系)。线性绝对值不等式域是经典多面体域的一般化，虽然表达能力与区间多面体域相同，但是其域操作都是具体域上对应操作的最佳抽象。而线性绝对值等式域是经典仿射等式域的一般化。基于广义线性互补系统的双重描述法并采用多精度有理数实现了这两个抽象域。
本文提出的数值抽象域在分析精度和计算效率间进行了不同的权衡，可以面向不同的应用。这些抽象域都在数值抽象域库APRON中得以实现，并且实验结果令人鼓舞。
Trustworthiness of software has become the center of attention when consider-ing modern software quality. Finding bugs before release is fundamental to buildtrustworthy software, which is extremely important for safety-critical applicationssuch as aerospace, defense and automotive. Scienti?c and engineering programs es-pecially safety-critical embedded software are usually related to mathematics andphysics, and thus often involve a lot of numerical computations. Hence, many pro-gram bugs including division by zero, arithmetic over?ows and array out-of-bounds,are closely related to numerical properties in the program.
Abstract interpretation is a theory of semantics approximation, allowing thedesign of sound and e?cient static analyses. Abstract domains are a key ingredi-ent in this framework: They enable semantic choices (what properties to infer) andalgorithmic choices (how to compute). In this thesis, we focus on design and im-plementation of numerical abstract domains that are used to automatically discovernumerical properties over program variables. Over the past decades, a wide variety ofnumerical abstract domains have been proposed. However, most existing abstractdomains (especially relational ones) need arbitrary precision rational numbers tobuild implementations, which may degrade the time and memory e?ciency. Mostof them can only represent convex properties, and hence have limitations in deal-ing with disjunctions. Besides, currently there is no abstract domain that supportsinterval variable coe?cients which appear naturally in real-life program analysis.
The goal of this thesis is to explore more e?cient numerical abstract domains,using sound ?oating-point constructions, and to design more precise ones, allowingnon-convex properties and interval coe?cients.
Major contributions of this thesis are listed as follows.
1) We present a so-called ?oating-point polyhedra abstract domain. The clas-sical convex polyhedra domain is one of the most powerful and commonly used ab-stract domains in the ?eld, but rational implementations may su?er from scalabilityproblems. To solve this issue, we present an implementation using ?oating-pointarithmetic without sacri?cing soundness, based on a constraint-only representation using ?oating-point coe?cients. Since its complexity mainly comes from the costlyjoin operation (i.e., polyhedral convex hull), a series of cheap weak join operationsare then proposed.
2) We introduce interval linear algebra to static analysis and propose intervallinear abstract domains that support interval coe?cients. Intervals are naturallysuited to construct sound ?oating-point abstract domains. First, a so-called intervalpolyhedra domain is proposed to infer interval linear inequalities. Then, a restrictedabstract domain is proposed based on a system of interval linear equalities in rowechelon form, polynomial in time and memory. The two domains can be consid-ered as interval extensions of the existing convex polyhedra domain and the a?neequality domain respectively. By interpreting solutions as weak solutions of intervallinear systems, both domains can express certain non-convex (even unconnected)properties. They are soundly implemented using ?oating-point numbers based oninterval arithmetic with outward rounding.
3) We present linear absolute value abstract domains that natively allow toexpress non-convex properties. Absolute value (AV) is fundamental in mathematicsand often used to describe piecewise linear behavior. The equivalence among linearAV inequality systems, interval linear inequality systems and extended linear com-plementarity problem (XLCP) systems is stated. We construct a double descriptionmethod for XLCP on top of that for polyhedra, based on which a new method forsolving AV linear programming problems is shown. On this basis, we propose anabstract domain of linear AV equalities, and an abstract domain of linear AV in-equalities that has the same expressiveness as interval polyhedra domain but enjoysoptimal transfer functions. They are implemented using rational numbers based onthe double description method for XLCP.
The numerical abstract domains presented in this thesis provide di?erent trade-o?s between precision and e?ciency, and can be applied to di?erent problems. Theyare implemented in the APRON library, and experimental results are encouraging.
引文
[1]刘克，单志广，王戟，何积丰，张兆田，秦玉文．“可信软件基础研究”重大研究计划综述．中国科学基金．2008，22(3)：145-151．
[2] The Economist. Software that makes software better. The Economist TechnologyQuarterly. 8th March 2008:20-21.
[3] S. McConnell. Code Complete. Microsoft Press, 1993.
[4] NIST. Software errors costs U.S. economy $59.5 billion annually. Tech. Rep. NIST2002-10, National Institute of Standards and Technology, June 2002.
[5] R. Skeel. Roundoff error and the Patriot missile. SIAM News. July 1992, 25(4):11.
[6] J.L. Lions et al. Ariane 5 flight 501 failure report by the inquiry board. Tech. rep.,European Space Agency, Paris, FVance, 1996.
[7]梅宏，王千祥，张路，王戟．软件分析技术进展．计算机学报．2009，32(9)：1697- 1710．
[8] R.W. Floyd. Assigning Meaning to Programs. Proc. of Symposium on AppliedMathematics. American Mathematical Society, 1967, vol. 19, 19-32.
[9] C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communicationsof the ACM. 1969, 12(10):576-580.
[10] P. Naur. Proof of algorithms by general snapshots. BIT. 1966, 6(4).
[11] R. Gerth. Model Checking if Your Life Depends on It a View from Intel's Trenches.SPIN'01. Springer, 2001, vol. 2057 of LNCS, 15.
[12] T. Ball, S. K. Rajamani. The SLAM project: debugging system software via staticanalysis. ACM POPL02. ACM Press, 2002, 1-3.
[13] T. Ball, B. Cook, V. Levin, S. K. Rajamani. SLAM and Static Driver Verifier:Technology Transfer of Formal Methods inside Microsoft. IFM,04. Springer, 2004,vol. 2999 of LNCS, 1-20.
[14] B. Cook, A. Podelski, A. Rybalchenko. Terminator: Beyond Safety. CAV'06.Springer, 2006, vol. 4144 of LNCS, 415-418.
[15] T. Hoare, J. Misra. Verified Software: Theories, Tools, Experiments Vision ofa Grand Challenge Project. Verified Software: Theories, Tools, Experiments(VSTTE'05). Springer, 2008, vol. 4171 of LNCS, 1-18.
[16] C. B. Jones, P. W. O'Hearn, J. Woodcock. Verified Software: A Grand Challenge.IEEE Computer. 2006, 39(4):93-95.
[17] D. Jackson. Dependable Software by Design. Scientific American. June, 294(6).
[18] G. Stix. Send in the Terminator. Scientific American. December 2006, 294(12).
[19] H.G. Rice. Classes of Recursively Enumerable Sets and Their Decision Problems.Transactions of the American Mathematical Society. 1953, 74(2):358-366.
[20] P. Cousot, R. Cousot. Abstract interpretation: a unified lattice model for staticanalysis of programs by construction or approximation of fixpoints. ACM POPI/77.ACM Press, New York, 1977, 238-252.
[21] B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux,X. Rival. A Static Analyzer for Large Safety-Critical Software. ACM PLDI'03).ACM Press, 2003, 196-207.
[22] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux, X. Rival.The ASTREE Analyzer. ESOP'05. Springer, 2005, vol. 3444 of LNCS, 21-30.
[23] The MathWorks. Polyspace Products for Embedded Software Verification.http://www.mathworks.com/products/polyspace/.
[24] E. Goubault, M. Martel, S. Putot. Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter. ESOP'02. Springer, 2002, vol. 2305 ofLNCS, 209-212.
[25] D. Delmas, E. Goubault, S. Putot, J. Souyris, K. Tekkal, F. Vedrine. Towardsan Industrial Use of FLUCTUAT on Safety-Critical Avionics Software. FMICS'09.Springer, 2009, vol. 5825 of LNCS, 53-69.
[26] O. Bouissou, E. Conquet, P. Cousot, R. Cousot, J. Feret, K. Ghorbal, E. Goubault,D. Lesens, L. Mauborgne, A. Mine, S. Putot, X. Rival, M. Ttorin. Space SoftwareValidation using Abstract Interpretation. DASIA'09. ESA, 2009, vol. SP-669, 1-7.
[27] D. Delmas, J. Souyris. Astree: FVom Research to Industry. SAS'07. Springer, 2007,vol. 4634 of LNCS, 437-451.
[28] J. Souyris, D. Delmas. Experimental Assessment of Astree on Safety-Critical Avionics Software. SAFECOMP'07. Springer, 2007, vol. 4680 of LNCS, 479-490.
[29] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, X. Rival. Why does Astreescale up? Formal Methods in System Design. 2010, 35(3):229-264.
[30] P. Cousot. The Verification Grand Challenge and Abstract Interpretation. VerifiedSoftware: Theories, Tools, Experiments (VSTTE,05). Springer, 2008, vol. 4171 ofLNCS, 189-201.
[31] D. Wagner, J. S. Foster, E. A. Brewer, A. Aiken. A First Step Towards AutomatedDetection of Buffer Overrun Vulnerabilities. NDSS'00. The Internet Society, 2000.
[32] D. Brumley, T. Chiueh, R. Johnson, H. Lin, D. Song. RICH: Automatically Protecting Against Integer-Based Vulnerabilities. NDSS'07. The Internet Society, 2007.
[33] N. Dor, M. Rodeh, S. Sagiv. CSSV: towards a realistic tool for statically detectingall buffer overflows in C. PLDP03. ACM Press, 2003, 155-167.
[34] V. Ganapathy, S. Jha, D. Chandler, D. Melski, D. Vitek. Buffer overrun detectionusing linear programming and static analysis. CCS'03. ACM Press, 2003.
[35] R. Rugina, M. C. Rinard. Symbolic bounds analysis of pointers, array indices,and accessed memory regions. ACM Transactions on Programming Languages andSystems (TOPLAS). 2005, 27(2): 185-235.
[36] X. Allamigeon, W. Godard, C. Hymans. Static Analysis of String Manipulations inCritical Embedded C Programs. SAS'06. Springer, 2006, vol. 4134 of LNCS, 35-51.
[37] G. Kildall. A Unified Approach to Global Program Optimization. ACM POPL,73.ACM Press, 1973, 194-206.
[38] P. Cousot, R. Cousot. Static determination of dynamic properties of programs.Proc. of the 2nd International Symposium on Programming. Dunod, Paris, 1976,106-130.
[39] M. Karr. Affine Relationships Among Variables of a Program. Acta Inf. 1976,6:133-151.
[40] P. Cousot, N. Halbwachs. Automatic discovery of linear restraints among variablesof a program. ACM POPL'78. ACM Press, New York, 1978, 84-96.
[41] A. Mine. The Octagon Abstract Domain. Higher-Order and Symbolic Computation.2006, 19(l):31-100.
[42] A. Mine Weakly Relational Numerical Abstract Domains. Ph.D. thesis, EcolePolytechnique, Palaiseau, France, December 2004.
[43] S. Sankaranarayanan. Mathematical Analysis of Programs. Ph.D. thesis, StanfordUniversity, Stanford, CA, USA, September 2005.
[44] D. Gopan. Numeric program analysis techniques with applications to array analysisand library summarization. Ph.D. thesis, University of Wisconsin, Madison, WI,USA, August 2007.
[45] M. Colon, H. Sipma. Synthesis of Linear Ranking Functions. TACAS'01. Springer,2001, vol. 2031 of LNCS, 67-81.
[46] M. Col6n, H. Sipma. Practical Methods for Proving Program Termination. CAV'02.Springer, 2002, vol. 2404 of LNCS, 442-454.
[47] Y. Chen, B. Xia, L. Yang, N. Zhan, C. Zhou. Discovering Non-linear RankingFunctions by Solving Semi-algebraic Systems. ICTAC'07. Springer, 2007, vol. 4711of LNCS, 34-49.
[48] J. Berdine. A. Chawdhary, B. Cook, D. Distefano, P. W. O'Hearn. Variance analysesfrom invariance analyses. 34th ACM Symposium on Principles of ProgrammingLanguages (POPL'07). ACM Press, New York, 2007, 211-224.
[49] A. Chawdhary, B. Cook, S. Gulwani, M. Sagiv, H. Yang. Ranking Abstractions.the 17th European Symposium on Programming (ESOP'08). Springer-Verlag, 2008,vol. 4960 of LNCS, 148-162.
[50] B. S. Gulavani, S. Gulwani. A Numerical Abstract Domain based on ExpressionAbstraction and Max Operator with Application in Timing Analysis. CAV'08.Springer-Verlag, 2008, vol. 5123 of LNCS, 370-384.
[51] S. Gulwani, S. Jain, E. Koskinen. Control-flow refinement and progress invariantsfor bound analysis. ACM PLDI'09. ACM Press, 2009, 375-385.
[52] S. Gulwani, T. Lev-Ami, M. Sagiv. A combination framework for tracking partitionsizes. ACM POPL'09. ACM Press, 2009, 239-251.
[53] S. Gulwani, K. K. Mehra, T. M. Chilimbi. SPEED: precise and efficient staticestimation of program computational complexity. ACM POPL'09. ACM Press,2009, 127-139.
[54] S. Gulwani. SPEED: Symbolic Complexity Bound Analysis. CAV'09. Springer,2009, vol. 5643 of LNCS, 51-62.
[55] R. Rugina. Quantitative Shape Analysis. SAS'04. Springer, 2004, vol. 3148 of LNCS,228-245.
[56] S. Magill, J. Berdine, E. M. Clarke, B. Cook. Arithmetic Strengthening for ShapeAnalysis. SAS'07. Springer, 2007, vol. 4634 of LNCS, 419-436.
[57] S. Magill, M. Tsai, P. Lee, Y. Tsay. Automatic numeric abstractions for heap-manipulating programs. ACM POPL'10. ACM Press, 2010, 211-222.
[58] B.-Y. E. Chang, X. Rival. Relational inductive shape analysis. ACM POPL,08.ACM Press, 2008.
[59] V. D'Silva, D. Kroening, G. Weissenbacher. A Survey of Automated Techniquesfor Formal Software Verification. IEEE Transactions on Computer-Aided Design ofIntegrated Circuits and Systems (TCAD). 2008, 27(7):1165-1178.
[60] R. Jhala, R. Majumdar. Software model checking. ACM Computing Surveys. 2009,41(4).
[61] David A. Schmidt. Data Flow Analysis is Model Checking of Abstract Interpreta-tions. ACM POPL'98. ACM Press, 1998, 38-48.
[62] D. A. Schmidt, B. Steffen. Program Analysis $ Model Checking of Abstract Interpretations. SAS'98. Springer, 1998, vol. 1503 of LNCS, 351-380.(63] A. Gurfinkel, S. Chaki. Combining Predicate and Numeric Abstraction for Software Model Checking. FMCAD'08. IEEE, 2008, 1-9.
[64] S. Chaki, A. Gurfinkel, O. Strichman. Decision diagrams for linear arithmetic. FMCAD'09. IEEE, 2009, 53-60.
[65] H. Jain, F. Ivancic, A. Gupta, I. Shlyakhter, C. Wang. Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. CAV'06. Springer, 2006, vol. 4144 of LNCS, 137-151.
[66] G. Goth. Exploring new frontiers. Communications of the ACM. 2009, 52(11):21-23.
[67] Dr. Dobb's Journal. Computing Luminaries Receive NSF Grant To Develop Modeling Tools for Complex Systems. August 19, 2009.
[68] A. Mine. A New Numerical Abstract Domain Based on Difference-Bound Matrices. Proc. of the 2d Symp. on Programs as Data Objects (PADO II). Springer, 2001, vol. 2053 of LNCS, 155-172.
[69] K. G. Larsen, F. Larsson, P. Pettersson, W. Yi. Efficient verification of real-time systems: compact data structure and state-space reduction. IEEE Real-Time Systems Symposium. IEEE Computer Society, 1997, 14-24.
[70] S. Yovine. Model-checking timed automata. Lectures on Embedded Systems. The Internet Society, 1998, vol. 1494 of LNCS, 25-41.
[71] K. G. Larsen, P. Pettersson, Y. Wang. UPPAAL in a Nutshell. Int J Softw Tools Technol Ttansf (STTT). 1997, 1(1-2):134-152.
[72] M. Bozga, C. Daws, O. Maler, A. Olivero, S. TWpakis, S. Yovine. Kronos: A Model-Checking Tool for Real-Time Systems. CAV'98. Springer, 1998, vol. 1427 of LNCS, 546-550.
[73] T. A. Henzinger, P.-H. Ho, H. Wong-Toi. HYTECH: A Model Checker for Hybrid Systems. Int J Softw Tools Technol Ttansf (STTT). 1997, l(l-2):110-122.
[74] N. Halbwachs, Y.-E. Proy, P. Roumanoff. Verification of Real-Time Systems using Linear Relation Analysis. Formal Methods in System Design. 1997, 11(2):157-185.
[75] G. FVehse. PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. Int J Softw Tools Technol Ttansf (STTT). 2008, 10(3):263-279.
[76] O. Bournez, O. Maler, A. Pnueli. Orthogonal Polyhedra: Representation and Com-putation. HSCC'99. Springer, 1999, vol. 1569 of LNCS, 46-60.
[77] E. Asarin, T. Dang, O. Maler. The d/dt Tool for Verification of Hybrid Systems.CAV'02. Springer, 2002, vol. 2404 of LNCS, 365-370.
[78] A. Girard. Reachability of Uncertain Linear Systems Using Zonotopes. HSCC.Springer, 2005, vol. 3414 of LNCS, 291-305.
[79] S. Sankaranarayanan, T. Dang, F. Ivancic. Symbolic Model Checking of HybridSystems Using Template Polyhedra. TACAS,08. Springer, 2008, vol. 4963 of LNCS,188-202.
[80] P. Cousot, R. Cousot. Systematic design of program analysis frameworks. ACMPOPL'79. ACM Press, New York, 1979, 269-282.
[81] GNU Multiple Precision arithmetic library, http://gmplib.org/.
[82] A. Simon, A. King. Exploiting Sparsity in Polyhedral Analysis. SAS'05. SpringerVerlag, 2005, vol. 3672 of LNCS, 336-351.
[83] D. N. Que. Robust and Generic Abstract Domain for Static Program Analysis: thePolyhedral Case. Tech. rep., ficole des Mines de Paris, July 2006.
[84] A. Mine. Relational Abstract Domains for the Detection of Float ing-Point RunTime Errors. ESOP'04. Springer, 2004, vol. 2986 of LNCS, 3-17.
[85] A. Mine. Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. VMCAI'Oe. Springer, 2006, vol. 3855 of LNCS, 348-363.
[86] APRON numerical abstract domain library. Http://apron.cri.ensmp.fr/library/.
[87] G. Lalire, M. Argoud, B. Jeannet. Interproc. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/.
[88] R. Bagnara, P. M. Hill, E. Zaffanella. Applications of Polyhedral Computationsto the Analysis and Verification of Hardware and Software Systems. TheoreticalComputer Science. 2009, 410(46):4672-4691.
[89] R. Clariso, J. Cortadellab. The octahedron abstract domain. Science of ComputerProgramming. 2007, 64(1):115-139.
[90] A. Simon, A. King, J. M. Howe. Two Variables per Linear Inequality as an AbstractDomain. LOPSTR'03. Springer, 2003, vol. 2664 of LNCS, 71-89.
[91] S. Sankaranarayanan, H. Sipma, Z. Manna. Scalable Analysis of Linear Systemsusing Mathematical Programming. VMCAI'05. Springer Verlag, 2005, vol. 3385 ofLNCS, 25-41.
[92] S. Sankaranarayanan, F. Ivancic, A. Gupta. Program Analysis Using SymbolicRanges. SAS'07. Springer, 2007, vol. 4634 of LNCS, 366-383.
[93] F. Logozzo, M. Fahndrich. Pentagons: a weakly relational abstract domain for theefficient validation of array accesses. ACM SAC'08. ACM Press, 2008, 184-188. [94] V. Laviron, F. Logozzo. SubPolyhedra: A (more) scalable approach to infer linearinequalities. VMCAI'09. Springer Verlag, 2009, vol. 5403 of LNCS, 229-244. [95] J. Feret. Static Analysis of Digital Filters. ESOP'04. No. 2986 in LNCS, Springer-Verlag, 2004. [96] J. Feret. The Arithmetic-Geometric Progression Abstract Domain. VMCAI'05. No.3385 in LNCS, Springer-Verlag, 2005, 42-58.
[97] P. Cousot, R. Cousot. Higher-Order Abstract Interpretation (and Application toComportment Analysis Generalizing Strictness, Termination, Projection and PERAnalysis of Functional Languages). ICCL,94. IEEE Computer Society Press, 1994,95-112.
[98] R. Giacobazzi, F. Ranzato. Optimal domains for disjunctive abstract interpretation.Sci Comput Program. 1998, 32(l-3):177-210.
[99] R. Bagnara, P. M. Hill, E. Zaffanella. Widening operators for powerset domains.VMCAT04. Springer Verlag, 2004, vol. 2937 of LNCS, 135-148.
[100] X. Rival, L. Mauborgne. The Trace Partitioning Abstract Domain. ACM Transactions on Programming Languages and Systems (TOPLAS). 2007, 29(5).
[101] S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, A. Gupta. Static Analysis in Disjunctive Numerical Domains. SAS'06. Springer, 2006, vol. 4134 of LNCS, 3-17.
[102] B. Jeannet. Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems. Formal Methods in System Design. 2003, 23(1):5-37.
[103] A. Simon. Splitting the Control Flow with Boolean Flags. SAS'08. Springer, 2008,vol. 5079 of LNCS, 315-331.
[104] P. Granger. Static analysis of arithmetical congruences. International Journal ofComputer Mathematics. 1989, 30:165-199.
[105] X. Allamigeon, S. Gaubert, E. Goubault. Inferring Mia and Max Invariants UsingMax-plus Polyhedra. SAS'08. Springer Verlag, 2008, vol. 5079 of LNCS, 189-204.
[106] J. ZHANG, Y. FENG. Obtaining exact value by approximate computations. Sciencein China Series A: Mathematics. 2007, 50(9): 1361-1368.
[107] A. Neumaier, O. Shcherbina. Safe bounds in linear and mixed-integer linear programming. Math Program. 2004, 99(2):283-296.
[108] C. Jansson. Rigorous Lower and Upper Bounds in Linear Programming. SIAMJournal on Optimization. 2004, 14(3):914-935.
[109] C. Jansson, D. Chaykin, C. Keil. Rigorous Error Bounds for the Optimal Value in Semidefinite Programming. SIAM Journal on Numerical Analysis. 2007, 46(l):180-200.
[110] C. Jansson. On Verified Numerical Computations in Convex Programming. Japan J Indust Appl Math. 2009, 26:337-363.
[111] D. Monniaux. On using floating-point computations to help an exact linear arithmetic decision procedure. CAV'09. Springer Verlag, 2009, vol. 5643 of LNCS, 570-583.
[112] David Goldberg. What Every Computer Scientist Should Know About Floatingpoint Arithmetic. ACM Computing Surveys. 1991, 23(1):5-48.
[113] D. Monniaux. The pitfalls of verifying floating-point computations. ACM Transactions on Programming Languages and Systems (TOPLAS). 2008, 30(3):l-41.
[114] V.R. Pratt. Anatomy of the Pentium Bug. TAPSOFT'95. Springer, 1995, vol. 915 of LNCS, 97-107.
[115] J. Harrison. Floating-Point Verification Using Theorem Proving. SFM'06. Springer,2006, vol. 3965 of LNCS, 211-242.
[116] J. Harrison. Floating-Point Verification. Journal of Universal Computer Science.2007, 13(5):629-638.
[117] E. Goubault. Static Analyses of Floating-Point Operations. SAS'01. Springer-Verlag, 2001, vol. 2126 of LNCS, 234-259.
[118] S. Boldo, J.-C. Filliatre. Formal Verification of Floating-Point Programs. 18th IEEE Symposium on Computer Arithmetic. IEEE Computer Society, 2007, 187-194.
[119] S. Boldo, J.-C. Filliatre, G. Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning. Springer, 2009, vol. 5625 of LNAI, 59-74.
[120] R. Moore. Interval Analysis. Prentice-Hall, 1966.
[121] B. Hayes. A lucid interval. American Scientist. 2003, 91(6):484-488.
[122] E. R. Hansen. Global Optimization Using Interval Analysis. New York, NY: Marcel Dekker, 1S92.
[123] L. Jaulin, M. Kieffer, O. Didrit, E. Walter. Applied Interval Analysis. London: Springer-Verlag, 2001.
[124] R. B. Kearfott. Interval Computations: Introduction, Uses, and Resources. Euro-math Bulletin. 1994, 1(2).
[125] A. Neumaier. Interval Methods for Systems of Equations. Cambridge UniversityPress, 1990.
[126] M. Fiedler, J. Nedoma, J. Ramfk, J. Rohn, K. Zimmermann. Linear optimizationproblems with inexact data. New York: Springer, 2006.
[127] W. Oettli, W. Prager. Compatibility of approximate solution of linear equationswith given error bounds for coefficients and right-hand sides. Numer Math. 1964,6:405-409.
[128] J. Rohn. A Handbook of Results on Interval Linear Problems. Tech. rep., CzechAcademy of Sciences, Prague, Czech Republic, April 2005.
[129] J. Rohn. Solvability of systems of interval linear equations and inequalities. LinearOptimization Problems with Inexact Data. Springer, 2006, 35-77.
[130] C. Jansson. Calculation of exact bounds for the solution set of linear interval systems. Linear Algebra and Its Applications. 1997, 251:321-340.
[131] J.W. Chineck, K. Ramadan. Linear Programming with interval coefficients. Journalof the Operational Research Society. 2000, 51(2):209-220.
[132] P. Cousot. Abstract interpretation. MIT course 16.399, Feb.-May 2005.http://web.mit.edu/16.399/www/.
[133] A. Tarski. A lattice-theoretical fixpoint theorem and its application. Pacific Journalof Mathematics. 1955, 5:285-309.
[134] P. Cousot, R. Cousot. Constructive Versions of Tarski's Fixed Point Theorems.Pacific Journal of Mathematics. 1979, 81(1):43-57.
[135] S.C. Kleene. Introduction to metamathematics. Amsterdam: North-Holland.
[136] Z. Su, D. Wagner. A class of polynomially solvable range constraints for intervalanalysis without widenings. Theor Comput Sci. 2005, 345(1):122-138.
[137] T. Gawlitza, J. Leroux, J. Reineke, H. Seidl, G. Sutre, R. Wilhplm. PolynomialPrecise Interval Analysis Revisited. Efficient Algorithms: Essays Dedicated to KurtMehlhorn on the Occasion of His 60th Birthday. Springer, 2009, vol. 5760 of LNCS,422-437.
[138] A. Costan, S.Gaubert, E.Goubault, M.Martel, S.Putot. A Policy iteration algorithmfor computing fixed points in static analysis of programs. CAV'05. Springer Verlag,2005, vol. 3576 of LNCS, 462-475.
[139] S. Gaubert, E. Goubault, A. Taly, S. Zennou. Static Analysis by Policy Iterationon Relational Domains. ESOP'07. Springer, 2007, vol. 4421 of LNCS, 237-252.
[140] T. Gawlitza, H. Seidl. Precise Relational Invariants Through Strategy Iteration.CSL'07. Springer, 2007, vol. 4646 of LNCS, 23-40.
[141] P. Cousot, R. Cousot. Comparing the Galois Connection and Widening/NarrowingApproaches to Abstract Interpretation. PLILP,92. Springer-Verlag, 1992, vol. 631of LNCS, 269-295.
[142] F. Bourdoncle. Efficient Chaotic Iteration Strategies with Widenings. FMPA'93.Springer Verlag, 1993, vol. 735 of LNCS, 128-141.
[143] F. Masdupuy. Array abstractions using semantic analysis of trapezoid congruences.ICS'92. ACM Press, 1992, 226-235.
[144] R. Bagnara, K. Dobson, P. M. Hill, M. Mundell, E. Zaffanella. Grids: A Domainfor Analyzing the Distribution of Numerical Values. LOPSTR'06. Springer-Verlag,2007, vol. 4407 of LNCS, 219-235.
[145]陈立前，王戟，侯苏宁．单变量区间线性不等式抽象域．计算机学报．2010，33(3)：427-439．
[146] J.M. Howe, A. King. Logahedra: a New Weakly Relational Domain. ATVA'09.Springer-Verlag, 2009, vol. 5799 of LNCS, 306-320.
[147] L. Chen, A. Mine, J. Wang, P. Cousot. An Abstract Domain to Discover IntervalLinear Equalities. VMCAI'10. Springer, 2010, vol. 5944 of LNCS, 112-128.
[148] P. Granger. Static analysis of linear congruence equalities among variables of aprogram. TAPSOFT'91. Springer-Verlag, 1991, vol. 493 of LNCS, 169-192.
[149] L. Chen, A. Mine, P. Cousot. A Sound Float ing-Point Polyhedra Abstract Domain.APLAS'08. Springer Verlag, 2008, vol. 5356 of LNCS, 3-18.
[150] L. Chen, A. Mine, J. Wang, P. Cousot. Interval Polyhedra: An Abstract Domainto Infer Interval Linear Relationships. SAS'09. Springer Verlag, 2009, vol. 5673 ofLNCS, 309-325.
[151] C. Bartzis, T. Bultan. Efficient Symbolic Representations for Arithmetic Constraintsin Verification. International Journal of Foundations of Computer Science. 2003,14(4):605-624.
[152] C. Bartzis, T. Bultan. Widening Arithmetic Automata. CAV'04. Springer, 2004,vol. 3114 of LNCS, 321-333.
[153] J. Leroux. Convex Hull of Arithmetic Automata. SAS'08. Springer, 2008, vol. 5079of LNCS, 47-61.
[154] R. Bagnara, P. M. Hill, E. Zaffanella. Not necessarily closed convex polyhedra andthe double description method. Formal Aspects of Computing. 2005,17(2):222-257.
[155] IEEE Computer Society. IEEE standard for binary floating point arithmetic. Tech.rep., ANSI/IEEE Std 745-1985, 1985.
[156] P. Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Electronic Notes in Theoretical Computer Science. 1997, 6.
[157] V. Loechner. PolyLib: A Library for Manipulating Parameterized Polyhedra. Available at http://icps.u-strasbg.fr/polylib/. mar 1000.
[158] B. Jeannet, A. Mine. Apron: A Library of Numerical Abstract Domains for Static Analysis. CAV'09. Springer, 2009, vol. 5643 of LNCS, 661-667.
[159] R. Bagnara, P. M. Hill, E. Zaffanella. The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. Science of Computer Programming. 2008, 72(l-2):3-21.
[160] H. LeVerge. A note on Chernikova's algorithm. Tech. Rep. 635, IRISA, France, 1992.
[161] N. Halbwachs. Determination automatique de relations line"aires verifiees par les variables d'un programme. Ph.D. thesis, These de 3eme cycle d'informatique, Uni-versite scientifique et medicale de Grenoble, Grenoble, FVance, March 1979.
[162] T. Huynh, C. Lassez, J.-L. Lassez. Practical Issues on the Projection of Polyhedral Sets. Annals of Mathematics and Artificial Intelligence. 1992, 6(4):295-315.
[163] J.-L. Imbert. Fourier's Elimination: Which to Choose? PCPP'93. 1993, 117-129.
[164] S. Sankaranarayanan, M. Col6n, H. B. Sipma, Z. Manna. Efficient Strongly Relational Polyhedral Analysis. VMCAT06. Springer, 2006, vol. 3855 of LNCS, 111-125.
[165] A. Makhorin. The GNU Linear Programming Kit, 2000.Http://www.gnu.org/software/glpk/.
[166] S. Sankaranarayanan, H. B. Sipma, Z. Manna. Constraint-Based Li near-Relations Analysis. SAS'04. Springer, 2004, vol. 3148 of LNCS, 53-68.
[167] M. Muller-Olm, H. Seidl. Precise interprocedural analysis through linear algebra. ACM POPL'04. ACM Press, 2004, 330-341.
[168] S. Gulwani, G. Necula. Discovering Affine Equalities Using Random Interpretation. ACM POPL'03. ACM Press, 2003, 74-84.
[169] M. Muller-Olm, H. Seidl. A Note on Karr's Algorithm. ICALP,04. Springer, 2004, vol. 3142 of LNCS, 1016-1028.
[170] R.W. Cottle, J.-S. Pang, R.E. Stone. The Linear Complementarity Problem. New York: Academic Press, 1992.
[171] B. De Schutter, B. De Moor. The extended linear complementarity problem. Math-ematical Programming. 1995, 71(3):289-325.
[172] W. P. M. H. Heemels, J. M. Schumacher, S. Weiland. Linear ComplementaritySystems. SIAM Journal on Applied Mathematics. 2000, 60(4):1234-1269.
[173] B. De Schutter, B. De Moor. The extended linear complementarity problem andits applications in the analysis and control of discrete event systems and hybridsystems. SISCTA'97. 1997, 394-398.
[174] B. De Schutter. The extended linear complementarity problem and its applicationsin analysis and control of discrete-event systems. Pareto Optimality, Game Theoryand Equilibria. Springer, 2008, vol. 17 of Springer Optimization and Its Applications,541-570.
[175] J. Rohn. A theorem of the alternatives for the equation Ax + B\x\ = 6. Linear andMultilinear Algebra. 2004, 52(6):421-426.
[176] L. Mangasarian, R.R. Meyer. Absolute Value Equations. Linear Algebra and ItsApplications. 2006, 419:359-367.
[177] L. Mangasarian. Absolute Value Programming. Computational Optimization andApplications. 2007, 36(l):43-53.
[178] J. Rohn. An Algorithm for Solving the Absolute Value Equation. Electronic Journalof Linear Algebra. 2009, 18:589-599.
[179] O.A. Prokopyev. On equivalent reformulations for absolute vlaue equations. Computational Optimization and Applications. 2009, 44(3):363-372.
[180] M. Anitescu, G. Lesaja, F.A. Potra. Equivaence between different formulations ofthe linear complementarity promblem. Optimization Methods and Software. 1997,7(3):265-290.
[181] B.C. Eaves, C.E. Lemke. Equivalence of LCP and PLS. MATHEMATICS OFOPERATIONS RESEARCH. 1981, 6(4):475-484.
[182] O. L. Mangasarian, J. S. Pang. The Extended Linear Complementarity Problem.SIAM J Matrix Anal Appl. 1995, 16(2):359-368.
[183] M.S. Gowda. On the extended linear complementarity problem. Math Program.1996, 72(l):33-50.
[184] T. S. Motzkin, H. Raiffa, G. L. Thompson, R. M. Thrall. The double descriptionmethod. Contributions to the Theory of Games. Princeton University Press, 1953,vol. 17 of Annals of Mathematics Studies, 51-73.
[185] A. Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc.,1986.
[186] K. Fukuda, A. Prodon. Double Description Method Revisited. Combinatorics and Computer Science. Springer, 1996, vol. 1120 of LNCS, 91-111.
[187] N.V. Chernikova. Algorithm for Finding a General Formula for the Non-Negative Solutions of a System of Linear equations. USSR Computational Mathematics and Mathematical Physics. 1964, 4(4):151-158.
[188] N.V. Chernikova. Algorithm for Finding a General Formula for the Non-Negative Solutions of a System of Linear Inequalities. USSR Computational Mathematics and Mathematical Physics. 1965, 5(2):228-233.
[189] N.V. Chernikova. Algorithm for discovering the set of all the solutions of a linear programming problem. USSR Computational Mathematics and Mathematical Physics. 1968, 8(6):282-293.
[190] I. M. Bomze, M. Budinich, P. M. Pardalos, M. Pelillo. T\v maximum clique problem. Handbook of Combinatorial Optimization (Supplement Volume A). Kluwer Academic Publishers, 1999, 1-74.
[191] D. F. Shanno, R. L. Weil. 'Linear' Programming with Absolute-Value Functionals. Operations Research. 1971, 19(l):120-124.
[192] G. B. Dantzig, M. N. Thapa. Linear programming 1: introduction. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1997.
[193] B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, S. K. Rajamani. SYNERGY: a new algorithm for property checking. SIGSOFT FSE'06. ACM Press, 2006, 117-127.
[194] T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Lazy abstraction. ACM POPL'02. ACM Press, 2002, 58-70.
[2] The Economist. Software that makes software better. The Economist TechnologyQuarterly. 8th March 2008:20-21.
[3] S. McConnell. Code Complete. Microsoft Press, 1993.
[4] NIST. Software errors costs U.S. economy $59.5 billion annually. Tech. Rep. NIST2002-10, National Institute of Standards and Technology, June 2002.
[5] R. Skeel. Roundoff error and the Patriot missile. SIAM News. July 1992, 25(4):11.
[6] J.L. Lions et al. Ariane 5 flight 501 failure report by the inquiry board. Tech. rep.,European Space Agency, Paris, FVance, 1996.
[7]梅宏，王千祥，张路，王戟．软件分析技术进展．计算机学报．2009，32(9)：1697- 1710．
[8] R.W. Floyd. Assigning Meaning to Programs. Proc. of Symposium on AppliedMathematics. American Mathematical Society, 1967, vol. 19, 19-32.
[9] C. A. R. Hoare. An Axiomatic Basis for Computer Programming. Communicationsof the ACM. 1969, 12(10):576-580.
[10] P. Naur. Proof of algorithms by general snapshots. BIT. 1966, 6(4).
[11] R. Gerth. Model Checking if Your Life Depends on It a View from Intel's Trenches.SPIN'01. Springer, 2001, vol. 2057 of LNCS, 15.
[12] T. Ball, S. K. Rajamani. The SLAM project: debugging system software via staticanalysis. ACM POPL02. ACM Press, 2002, 1-3.
[13] T. Ball, B. Cook, V. Levin, S. K. Rajamani. SLAM and Static Driver Verifier:Technology Transfer of Formal Methods inside Microsoft. IFM,04. Springer, 2004,vol. 2999 of LNCS, 1-20.
[14] B. Cook, A. Podelski, A. Rybalchenko. Terminator: Beyond Safety. CAV'06.Springer, 2006, vol. 4144 of LNCS, 415-418.
[15] T. Hoare, J. Misra. Verified Software: Theories, Tools, Experiments Vision ofa Grand Challenge Project. Verified Software: Theories, Tools, Experiments(VSTTE'05). Springer, 2008, vol. 4171 of LNCS, 1-18.
[16] C. B. Jones, P. W. O'Hearn, J. Woodcock. Verified Software: A Grand Challenge.IEEE Computer. 2006, 39(4):93-95.
[17] D. Jackson. Dependable Software by Design. Scientific American. June, 294(6).
[18] G. Stix. Send in the Terminator. Scientific American. December 2006, 294(12).
[19] H.G. Rice. Classes of Recursively Enumerable Sets and Their Decision Problems.Transactions of the American Mathematical Society. 1953, 74(2):358-366.
[20] P. Cousot, R. Cousot. Abstract interpretation: a unified lattice model for staticanalysis of programs by construction or approximation of fixpoints. ACM POPI/77.ACM Press, New York, 1977, 238-252.
[21] B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux,X. Rival. A Static Analyzer for Large Safety-Critical Software. ACM PLDI'03).ACM Press, 2003, 196-207.
[22] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, D. Monniaux, X. Rival.The ASTREE Analyzer. ESOP'05. Springer, 2005, vol. 3444 of LNCS, 21-30.
[23] The MathWorks. Polyspace Products for Embedded Software Verification.http://www.mathworks.com/products/polyspace/.
[24] E. Goubault, M. Martel, S. Putot. Asserting the Precision of Floating-Point Computations: A Simple Abstract Interpreter. ESOP'02. Springer, 2002, vol. 2305 ofLNCS, 209-212.
[25] D. Delmas, E. Goubault, S. Putot, J. Souyris, K. Tekkal, F. Vedrine. Towardsan Industrial Use of FLUCTUAT on Safety-Critical Avionics Software. FMICS'09.Springer, 2009, vol. 5825 of LNCS, 53-69.
[26] O. Bouissou, E. Conquet, P. Cousot, R. Cousot, J. Feret, K. Ghorbal, E. Goubault,D. Lesens, L. Mauborgne, A. Mine, S. Putot, X. Rival, M. Ttorin. Space SoftwareValidation using Abstract Interpretation. DASIA'09. ESA, 2009, vol. SP-669, 1-7.
[27] D. Delmas, J. Souyris. Astree: FVom Research to Industry. SAS'07. Springer, 2007,vol. 4634 of LNCS, 437-451.
[28] J. Souyris, D. Delmas. Experimental Assessment of Astree on Safety-Critical Avionics Software. SAFECOMP'07. Springer, 2007, vol. 4680 of LNCS, 479-490.
[29] P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Mine, X. Rival. Why does Astreescale up? Formal Methods in System Design. 2010, 35(3):229-264.
[30] P. Cousot. The Verification Grand Challenge and Abstract Interpretation. VerifiedSoftware: Theories, Tools, Experiments (VSTTE,05). Springer, 2008, vol. 4171 ofLNCS, 189-201.
[31] D. Wagner, J. S. Foster, E. A. Brewer, A. Aiken. A First Step Towards AutomatedDetection of Buffer Overrun Vulnerabilities. NDSS'00. The Internet Society, 2000.
[32] D. Brumley, T. Chiueh, R. Johnson, H. Lin, D. Song. RICH: Automatically Protecting Against Integer-Based Vulnerabilities. NDSS'07. The Internet Society, 2007.
[33] N. Dor, M. Rodeh, S. Sagiv. CSSV: towards a realistic tool for statically detectingall buffer overflows in C. PLDP03. ACM Press, 2003, 155-167.
[34] V. Ganapathy, S. Jha, D. Chandler, D. Melski, D. Vitek. Buffer overrun detectionusing linear programming and static analysis. CCS'03. ACM Press, 2003.
[35] R. Rugina, M. C. Rinard. Symbolic bounds analysis of pointers, array indices,and accessed memory regions. ACM Transactions on Programming Languages andSystems (TOPLAS). 2005, 27(2): 185-235.
[36] X. Allamigeon, W. Godard, C. Hymans. Static Analysis of String Manipulations inCritical Embedded C Programs. SAS'06. Springer, 2006, vol. 4134 of LNCS, 35-51.
[37] G. Kildall. A Unified Approach to Global Program Optimization. ACM POPL,73.ACM Press, 1973, 194-206.
[38] P. Cousot, R. Cousot. Static determination of dynamic properties of programs.Proc. of the 2nd International Symposium on Programming. Dunod, Paris, 1976,106-130.
[39] M. Karr. Affine Relationships Among Variables of a Program. Acta Inf. 1976,6:133-151.
[40] P. Cousot, N. Halbwachs. Automatic discovery of linear restraints among variablesof a program. ACM POPL'78. ACM Press, New York, 1978, 84-96.
[41] A. Mine. The Octagon Abstract Domain. Higher-Order and Symbolic Computation.2006, 19(l):31-100.
[42] A. Mine Weakly Relational Numerical Abstract Domains. Ph.D. thesis, EcolePolytechnique, Palaiseau, France, December 2004.
[43] S. Sankaranarayanan. Mathematical Analysis of Programs. Ph.D. thesis, StanfordUniversity, Stanford, CA, USA, September 2005.
[44] D. Gopan. Numeric program analysis techniques with applications to array analysisand library summarization. Ph.D. thesis, University of Wisconsin, Madison, WI,USA, August 2007.
[45] M. Colon, H. Sipma. Synthesis of Linear Ranking Functions. TACAS'01. Springer,2001, vol. 2031 of LNCS, 67-81.
[46] M. Col6n, H. Sipma. Practical Methods for Proving Program Termination. CAV'02.Springer, 2002, vol. 2404 of LNCS, 442-454.
[47] Y. Chen, B. Xia, L. Yang, N. Zhan, C. Zhou. Discovering Non-linear RankingFunctions by Solving Semi-algebraic Systems. ICTAC'07. Springer, 2007, vol. 4711of LNCS, 34-49.
[48] J. Berdine. A. Chawdhary, B. Cook, D. Distefano, P. W. O'Hearn. Variance analysesfrom invariance analyses. 34th ACM Symposium on Principles of ProgrammingLanguages (POPL'07). ACM Press, New York, 2007, 211-224.
[49] A. Chawdhary, B. Cook, S. Gulwani, M. Sagiv, H. Yang. Ranking Abstractions.the 17th European Symposium on Programming (ESOP'08). Springer-Verlag, 2008,vol. 4960 of LNCS, 148-162.
[50] B. S. Gulavani, S. Gulwani. A Numerical Abstract Domain based on ExpressionAbstraction and Max Operator with Application in Timing Analysis. CAV'08.Springer-Verlag, 2008, vol. 5123 of LNCS, 370-384.
[51] S. Gulwani, S. Jain, E. Koskinen. Control-flow refinement and progress invariantsfor bound analysis. ACM PLDI'09. ACM Press, 2009, 375-385.
[52] S. Gulwani, T. Lev-Ami, M. Sagiv. A combination framework for tracking partitionsizes. ACM POPL'09. ACM Press, 2009, 239-251.
[53] S. Gulwani, K. K. Mehra, T. M. Chilimbi. SPEED: precise and efficient staticestimation of program computational complexity. ACM POPL'09. ACM Press,2009, 127-139.
[54] S. Gulwani. SPEED: Symbolic Complexity Bound Analysis. CAV'09. Springer,2009, vol. 5643 of LNCS, 51-62.
[55] R. Rugina. Quantitative Shape Analysis. SAS'04. Springer, 2004, vol. 3148 of LNCS,228-245.
[56] S. Magill, J. Berdine, E. M. Clarke, B. Cook. Arithmetic Strengthening for ShapeAnalysis. SAS'07. Springer, 2007, vol. 4634 of LNCS, 419-436.
[57] S. Magill, M. Tsai, P. Lee, Y. Tsay. Automatic numeric abstractions for heap-manipulating programs. ACM POPL'10. ACM Press, 2010, 211-222.
[58] B.-Y. E. Chang, X. Rival. Relational inductive shape analysis. ACM POPL,08.ACM Press, 2008.
[59] V. D'Silva, D. Kroening, G. Weissenbacher. A Survey of Automated Techniquesfor Formal Software Verification. IEEE Transactions on Computer-Aided Design ofIntegrated Circuits and Systems (TCAD). 2008, 27(7):1165-1178.
[60] R. Jhala, R. Majumdar. Software model checking. ACM Computing Surveys. 2009,41(4).
[61] David A. Schmidt. Data Flow Analysis is Model Checking of Abstract Interpreta-tions. ACM POPL'98. ACM Press, 1998, 38-48.
[62] D. A. Schmidt, B. Steffen. Program Analysis $ Model Checking of Abstract Interpretations. SAS'98. Springer, 1998, vol. 1503 of LNCS, 351-380.(63] A. Gurfinkel, S. Chaki. Combining Predicate and Numeric Abstraction for Software Model Checking. FMCAD'08. IEEE, 2008, 1-9.
[64] S. Chaki, A. Gurfinkel, O. Strichman. Decision diagrams for linear arithmetic. FMCAD'09. IEEE, 2009, 53-60.
[65] H. Jain, F. Ivancic, A. Gupta, I. Shlyakhter, C. Wang. Using Statically Computed Invariants Inside the Predicate Abstraction and Refinement Loop. CAV'06. Springer, 2006, vol. 4144 of LNCS, 137-151.
[66] G. Goth. Exploring new frontiers. Communications of the ACM. 2009, 52(11):21-23.
[67] Dr. Dobb's Journal. Computing Luminaries Receive NSF Grant To Develop Modeling Tools for Complex Systems. August 19, 2009.
[68] A. Mine. A New Numerical Abstract Domain Based on Difference-Bound Matrices. Proc. of the 2d Symp. on Programs as Data Objects (PADO II). Springer, 2001, vol. 2053 of LNCS, 155-172.
[69] K. G. Larsen, F. Larsson, P. Pettersson, W. Yi. Efficient verification of real-time systems: compact data structure and state-space reduction. IEEE Real-Time Systems Symposium. IEEE Computer Society, 1997, 14-24.
[70] S. Yovine. Model-checking timed automata. Lectures on Embedded Systems. The Internet Society, 1998, vol. 1494 of LNCS, 25-41.
[71] K. G. Larsen, P. Pettersson, Y. Wang. UPPAAL in a Nutshell. Int J Softw Tools Technol Ttansf (STTT). 1997, 1(1-2):134-152.
[72] M. Bozga, C. Daws, O. Maler, A. Olivero, S. TWpakis, S. Yovine. Kronos: A Model-Checking Tool for Real-Time Systems. CAV'98. Springer, 1998, vol. 1427 of LNCS, 546-550.
[73] T. A. Henzinger, P.-H. Ho, H. Wong-Toi. HYTECH: A Model Checker for Hybrid Systems. Int J Softw Tools Technol Ttansf (STTT). 1997, l(l-2):110-122.
[74] N. Halbwachs, Y.-E. Proy, P. Roumanoff. Verification of Real-Time Systems using Linear Relation Analysis. Formal Methods in System Design. 1997, 11(2):157-185.
[75] G. FVehse. PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. Int J Softw Tools Technol Ttansf (STTT). 2008, 10(3):263-279.
[76] O. Bournez, O. Maler, A. Pnueli. Orthogonal Polyhedra: Representation and Com-putation. HSCC'99. Springer, 1999, vol. 1569 of LNCS, 46-60.
[77] E. Asarin, T. Dang, O. Maler. The d/dt Tool for Verification of Hybrid Systems.CAV'02. Springer, 2002, vol. 2404 of LNCS, 365-370.
[78] A. Girard. Reachability of Uncertain Linear Systems Using Zonotopes. HSCC.Springer, 2005, vol. 3414 of LNCS, 291-305.
[79] S. Sankaranarayanan, T. Dang, F. Ivancic. Symbolic Model Checking of HybridSystems Using Template Polyhedra. TACAS,08. Springer, 2008, vol. 4963 of LNCS,188-202.
[80] P. Cousot, R. Cousot. Systematic design of program analysis frameworks. ACMPOPL'79. ACM Press, New York, 1979, 269-282.
[81] GNU Multiple Precision arithmetic library, http://gmplib.org/.
[82] A. Simon, A. King. Exploiting Sparsity in Polyhedral Analysis. SAS'05. SpringerVerlag, 2005, vol. 3672 of LNCS, 336-351.
[83] D. N. Que. Robust and Generic Abstract Domain for Static Program Analysis: thePolyhedral Case. Tech. rep., ficole des Mines de Paris, July 2006.
[84] A. Mine. Relational Abstract Domains for the Detection of Float ing-Point RunTime Errors. ESOP'04. Springer, 2004, vol. 2986 of LNCS, 3-17.
[85] A. Mine. Symbolic Methods to Enhance the Precision of Numerical Abstract Domains. VMCAI'Oe. Springer, 2006, vol. 3855 of LNCS, 348-363.
[86] APRON numerical abstract domain library. Http://apron.cri.ensmp.fr/library/.
[87] G. Lalire, M. Argoud, B. Jeannet. Interproc. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/.
[88] R. Bagnara, P. M. Hill, E. Zaffanella. Applications of Polyhedral Computationsto the Analysis and Verification of Hardware and Software Systems. TheoreticalComputer Science. 2009, 410(46):4672-4691.
[89] R. Clariso, J. Cortadellab. The octahedron abstract domain. Science of ComputerProgramming. 2007, 64(1):115-139.
[90] A. Simon, A. King, J. M. Howe. Two Variables per Linear Inequality as an AbstractDomain. LOPSTR'03. Springer, 2003, vol. 2664 of LNCS, 71-89.
[91] S. Sankaranarayanan, H. Sipma, Z. Manna. Scalable Analysis of Linear Systemsusing Mathematical Programming. VMCAI'05. Springer Verlag, 2005, vol. 3385 ofLNCS, 25-41.
[92] S. Sankaranarayanan, F. Ivancic, A. Gupta. Program Analysis Using SymbolicRanges. SAS'07. Springer, 2007, vol. 4634 of LNCS, 366-383.
[93] F. Logozzo, M. Fahndrich. Pentagons: a weakly relational abstract domain for theefficient validation of array accesses. ACM SAC'08. ACM Press, 2008, 184-188. [94] V. Laviron, F. Logozzo. SubPolyhedra: A (more) scalable approach to infer linearinequalities. VMCAI'09. Springer Verlag, 2009, vol. 5403 of LNCS, 229-244. [95] J. Feret. Static Analysis of Digital Filters. ESOP'04. No. 2986 in LNCS, Springer-Verlag, 2004. [96] J. Feret. The Arithmetic-Geometric Progression Abstract Domain. VMCAI'05. No.3385 in LNCS, Springer-Verlag, 2005, 42-58.
[97] P. Cousot, R. Cousot. Higher-Order Abstract Interpretation (and Application toComportment Analysis Generalizing Strictness, Termination, Projection and PERAnalysis of Functional Languages). ICCL,94. IEEE Computer Society Press, 1994,95-112.
[98] R. Giacobazzi, F. Ranzato. Optimal domains for disjunctive abstract interpretation.Sci Comput Program. 1998, 32(l-3):177-210.
[99] R. Bagnara, P. M. Hill, E. Zaffanella. Widening operators for powerset domains.VMCAT04. Springer Verlag, 2004, vol. 2937 of LNCS, 135-148.
[100] X. Rival, L. Mauborgne. The Trace Partitioning Abstract Domain. ACM Transactions on Programming Languages and Systems (TOPLAS). 2007, 29(5).
[101] S. Sankaranarayanan, F. Ivancic, I. Shlyakhter, A. Gupta. Static Analysis in Disjunctive Numerical Domains. SAS'06. Springer, 2006, vol. 4134 of LNCS, 3-17.
[102] B. Jeannet. Dynamic Partitioning in Linear Relation Analysis: Application to the Verification of Reactive Systems. Formal Methods in System Design. 2003, 23(1):5-37.
[103] A. Simon. Splitting the Control Flow with Boolean Flags. SAS'08. Springer, 2008,vol. 5079 of LNCS, 315-331.
[104] P. Granger. Static analysis of arithmetical congruences. International Journal ofComputer Mathematics. 1989, 30:165-199.
[105] X. Allamigeon, S. Gaubert, E. Goubault. Inferring Mia and Max Invariants UsingMax-plus Polyhedra. SAS'08. Springer Verlag, 2008, vol. 5079 of LNCS, 189-204.
[106] J. ZHANG, Y. FENG. Obtaining exact value by approximate computations. Sciencein China Series A: Mathematics. 2007, 50(9): 1361-1368.
[107] A. Neumaier, O. Shcherbina. Safe bounds in linear and mixed-integer linear programming. Math Program. 2004, 99(2):283-296.
[108] C. Jansson. Rigorous Lower and Upper Bounds in Linear Programming. SIAMJournal on Optimization. 2004, 14(3):914-935.
[109] C. Jansson, D. Chaykin, C. Keil. Rigorous Error Bounds for the Optimal Value in Semidefinite Programming. SIAM Journal on Numerical Analysis. 2007, 46(l):180-200.
[110] C. Jansson. On Verified Numerical Computations in Convex Programming. Japan J Indust Appl Math. 2009, 26:337-363.
[111] D. Monniaux. On using floating-point computations to help an exact linear arithmetic decision procedure. CAV'09. Springer Verlag, 2009, vol. 5643 of LNCS, 570-583.
[112] David Goldberg. What Every Computer Scientist Should Know About Floatingpoint Arithmetic. ACM Computing Surveys. 1991, 23(1):5-48.
[113] D. Monniaux. The pitfalls of verifying floating-point computations. ACM Transactions on Programming Languages and Systems (TOPLAS). 2008, 30(3):l-41.
[114] V.R. Pratt. Anatomy of the Pentium Bug. TAPSOFT'95. Springer, 1995, vol. 915 of LNCS, 97-107.
[115] J. Harrison. Floating-Point Verification Using Theorem Proving. SFM'06. Springer,2006, vol. 3965 of LNCS, 211-242.
[116] J. Harrison. Floating-Point Verification. Journal of Universal Computer Science.2007, 13(5):629-638.
[117] E. Goubault. Static Analyses of Floating-Point Operations. SAS'01. Springer-Verlag, 2001, vol. 2126 of LNCS, 234-259.
[118] S. Boldo, J.-C. Filliatre. Formal Verification of Floating-Point Programs. 18th IEEE Symposium on Computer Arithmetic. IEEE Computer Society, 2007, 187-194.
[119] S. Boldo, J.-C. Filliatre, G. Melquiond. Combining Coq and Gappa for Certifying Floating-Point Programs. 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning. Springer, 2009, vol. 5625 of LNAI, 59-74.
[120] R. Moore. Interval Analysis. Prentice-Hall, 1966.
[121] B. Hayes. A lucid interval. American Scientist. 2003, 91(6):484-488.
[122] E. R. Hansen. Global Optimization Using Interval Analysis. New York, NY: Marcel Dekker, 1S92.
[123] L. Jaulin, M. Kieffer, O. Didrit, E. Walter. Applied Interval Analysis. London: Springer-Verlag, 2001.
[124] R. B. Kearfott. Interval Computations: Introduction, Uses, and Resources. Euro-math Bulletin. 1994, 1(2).
[125] A. Neumaier. Interval Methods for Systems of Equations. Cambridge UniversityPress, 1990.
[126] M. Fiedler, J. Nedoma, J. Ramfk, J. Rohn, K. Zimmermann. Linear optimizationproblems with inexact data. New York: Springer, 2006.
[127] W. Oettli, W. Prager. Compatibility of approximate solution of linear equationswith given error bounds for coefficients and right-hand sides. Numer Math. 1964,6:405-409.
[128] J. Rohn. A Handbook of Results on Interval Linear Problems. Tech. rep., CzechAcademy of Sciences, Prague, Czech Republic, April 2005.
[129] J. Rohn. Solvability of systems of interval linear equations and inequalities. LinearOptimization Problems with Inexact Data. Springer, 2006, 35-77.
[130] C. Jansson. Calculation of exact bounds for the solution set of linear interval systems. Linear Algebra and Its Applications. 1997, 251:321-340.
[131] J.W. Chineck, K. Ramadan. Linear Programming with interval coefficients. Journalof the Operational Research Society. 2000, 51(2):209-220.
[132] P. Cousot. Abstract interpretation. MIT course 16.399, Feb.-May 2005.http://web.mit.edu/16.399/www/.
[133] A. Tarski. A lattice-theoretical fixpoint theorem and its application. Pacific Journalof Mathematics. 1955, 5:285-309.
[134] P. Cousot, R. Cousot. Constructive Versions of Tarski's Fixed Point Theorems.Pacific Journal of Mathematics. 1979, 81(1):43-57.
[135] S.C. Kleene. Introduction to metamathematics. Amsterdam: North-Holland.
[136] Z. Su, D. Wagner. A class of polynomially solvable range constraints for intervalanalysis without widenings. Theor Comput Sci. 2005, 345(1):122-138.
[137] T. Gawlitza, J. Leroux, J. Reineke, H. Seidl, G. Sutre, R. Wilhplm. PolynomialPrecise Interval Analysis Revisited. Efficient Algorithms: Essays Dedicated to KurtMehlhorn on the Occasion of His 60th Birthday. Springer, 2009, vol. 5760 of LNCS,422-437.
[138] A. Costan, S.Gaubert, E.Goubault, M.Martel, S.Putot. A Policy iteration algorithmfor computing fixed points in static analysis of programs. CAV'05. Springer Verlag,2005, vol. 3576 of LNCS, 462-475.
[139] S. Gaubert, E. Goubault, A. Taly, S. Zennou. Static Analysis by Policy Iterationon Relational Domains. ESOP'07. Springer, 2007, vol. 4421 of LNCS, 237-252.
[140] T. Gawlitza, H. Seidl. Precise Relational Invariants Through Strategy Iteration.CSL'07. Springer, 2007, vol. 4646 of LNCS, 23-40.
[141] P. Cousot, R. Cousot. Comparing the Galois Connection and Widening/NarrowingApproaches to Abstract Interpretation. PLILP,92. Springer-Verlag, 1992, vol. 631of LNCS, 269-295.
[142] F. Bourdoncle. Efficient Chaotic Iteration Strategies with Widenings. FMPA'93.Springer Verlag, 1993, vol. 735 of LNCS, 128-141.
[143] F. Masdupuy. Array abstractions using semantic analysis of trapezoid congruences.ICS'92. ACM Press, 1992, 226-235.
[144] R. Bagnara, K. Dobson, P. M. Hill, M. Mundell, E. Zaffanella. Grids: A Domainfor Analyzing the Distribution of Numerical Values. LOPSTR'06. Springer-Verlag,2007, vol. 4407 of LNCS, 219-235.
[145]陈立前，王戟，侯苏宁．单变量区间线性不等式抽象域．计算机学报．2010，33(3)：427-439．
[146] J.M. Howe, A. King. Logahedra: a New Weakly Relational Domain. ATVA'09.Springer-Verlag, 2009, vol. 5799 of LNCS, 306-320.
[147] L. Chen, A. Mine, J. Wang, P. Cousot. An Abstract Domain to Discover IntervalLinear Equalities. VMCAI'10. Springer, 2010, vol. 5944 of LNCS, 112-128.
[148] P. Granger. Static analysis of linear congruence equalities among variables of aprogram. TAPSOFT'91. Springer-Verlag, 1991, vol. 493 of LNCS, 169-192.
[149] L. Chen, A. Mine, P. Cousot. A Sound Float ing-Point Polyhedra Abstract Domain.APLAS'08. Springer Verlag, 2008, vol. 5356 of LNCS, 3-18.
[150] L. Chen, A. Mine, J. Wang, P. Cousot. Interval Polyhedra: An Abstract Domainto Infer Interval Linear Relationships. SAS'09. Springer Verlag, 2009, vol. 5673 ofLNCS, 309-325.
[151] C. Bartzis, T. Bultan. Efficient Symbolic Representations for Arithmetic Constraintsin Verification. International Journal of Foundations of Computer Science. 2003,14(4):605-624.
[152] C. Bartzis, T. Bultan. Widening Arithmetic Automata. CAV'04. Springer, 2004,vol. 3114 of LNCS, 321-333.
[153] J. Leroux. Convex Hull of Arithmetic Automata. SAS'08. Springer, 2008, vol. 5079of LNCS, 47-61.
[154] R. Bagnara, P. M. Hill, E. Zaffanella. Not necessarily closed convex polyhedra andthe double description method. Formal Aspects of Computing. 2005,17(2):222-257.
[155] IEEE Computer Society. IEEE standard for binary floating point arithmetic. Tech.rep., ANSI/IEEE Std 745-1985, 1985.
[156] P. Cousot. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation. Electronic Notes in Theoretical Computer Science. 1997, 6.
[157] V. Loechner. PolyLib: A Library for Manipulating Parameterized Polyhedra. Available at http://icps.u-strasbg.fr/polylib/. mar 1000.
[158] B. Jeannet, A. Mine. Apron: A Library of Numerical Abstract Domains for Static Analysis. CAV'09. Springer, 2009, vol. 5643 of LNCS, 661-667.
[159] R. Bagnara, P. M. Hill, E. Zaffanella. The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems. Science of Computer Programming. 2008, 72(l-2):3-21.
[160] H. LeVerge. A note on Chernikova's algorithm. Tech. Rep. 635, IRISA, France, 1992.
[161] N. Halbwachs. Determination automatique de relations line"aires verifiees par les variables d'un programme. Ph.D. thesis, These de 3eme cycle d'informatique, Uni-versite scientifique et medicale de Grenoble, Grenoble, FVance, March 1979.
[162] T. Huynh, C. Lassez, J.-L. Lassez. Practical Issues on the Projection of Polyhedral Sets. Annals of Mathematics and Artificial Intelligence. 1992, 6(4):295-315.
[163] J.-L. Imbert. Fourier's Elimination: Which to Choose? PCPP'93. 1993, 117-129.
[164] S. Sankaranarayanan, M. Col6n, H. B. Sipma, Z. Manna. Efficient Strongly Relational Polyhedral Analysis. VMCAT06. Springer, 2006, vol. 3855 of LNCS, 111-125.
[165] A. Makhorin. The GNU Linear Programming Kit, 2000.Http://www.gnu.org/software/glpk/.
[166] S. Sankaranarayanan, H. B. Sipma, Z. Manna. Constraint-Based Li near-Relations Analysis. SAS'04. Springer, 2004, vol. 3148 of LNCS, 53-68.
[167] M. Muller-Olm, H. Seidl. Precise interprocedural analysis through linear algebra. ACM POPL'04. ACM Press, 2004, 330-341.
[168] S. Gulwani, G. Necula. Discovering Affine Equalities Using Random Interpretation. ACM POPL'03. ACM Press, 2003, 74-84.
[169] M. Muller-Olm, H. Seidl. A Note on Karr's Algorithm. ICALP,04. Springer, 2004, vol. 3142 of LNCS, 1016-1028.
[170] R.W. Cottle, J.-S. Pang, R.E. Stone. The Linear Complementarity Problem. New York: Academic Press, 1992.
[171] B. De Schutter, B. De Moor. The extended linear complementarity problem. Math-ematical Programming. 1995, 71(3):289-325.
[172] W. P. M. H. Heemels, J. M. Schumacher, S. Weiland. Linear ComplementaritySystems. SIAM Journal on Applied Mathematics. 2000, 60(4):1234-1269.
[173] B. De Schutter, B. De Moor. The extended linear complementarity problem andits applications in the analysis and control of discrete event systems and hybridsystems. SISCTA'97. 1997, 394-398.
[174] B. De Schutter. The extended linear complementarity problem and its applicationsin analysis and control of discrete-event systems. Pareto Optimality, Game Theoryand Equilibria. Springer, 2008, vol. 17 of Springer Optimization and Its Applications,541-570.
[175] J. Rohn. A theorem of the alternatives for the equation Ax + B\x\ = 6. Linear andMultilinear Algebra. 2004, 52(6):421-426.
[176] L. Mangasarian, R.R. Meyer. Absolute Value Equations. Linear Algebra and ItsApplications. 2006, 419:359-367.
[177] L. Mangasarian. Absolute Value Programming. Computational Optimization andApplications. 2007, 36(l):43-53.
[178] J. Rohn. An Algorithm for Solving the Absolute Value Equation. Electronic Journalof Linear Algebra. 2009, 18:589-599.
[179] O.A. Prokopyev. On equivalent reformulations for absolute vlaue equations. Computational Optimization and Applications. 2009, 44(3):363-372.
[180] M. Anitescu, G. Lesaja, F.A. Potra. Equivaence between different formulations ofthe linear complementarity promblem. Optimization Methods and Software. 1997,7(3):265-290.
[181] B.C. Eaves, C.E. Lemke. Equivalence of LCP and PLS. MATHEMATICS OFOPERATIONS RESEARCH. 1981, 6(4):475-484.
[182] O. L. Mangasarian, J. S. Pang. The Extended Linear Complementarity Problem.SIAM J Matrix Anal Appl. 1995, 16(2):359-368.
[183] M.S. Gowda. On the extended linear complementarity problem. Math Program.1996, 72(l):33-50.
[184] T. S. Motzkin, H. Raiffa, G. L. Thompson, R. M. Thrall. The double descriptionmethod. Contributions to the Theory of Games. Princeton University Press, 1953,vol. 17 of Annals of Mathematics Studies, 51-73.
[185] A. Schrijver. Theory of linear and integer programming. John Wiley & Sons, Inc.,1986.
[186] K. Fukuda, A. Prodon. Double Description Method Revisited. Combinatorics and Computer Science. Springer, 1996, vol. 1120 of LNCS, 91-111.
[187] N.V. Chernikova. Algorithm for Finding a General Formula for the Non-Negative Solutions of a System of Linear equations. USSR Computational Mathematics and Mathematical Physics. 1964, 4(4):151-158.
[188] N.V. Chernikova. Algorithm for Finding a General Formula for the Non-Negative Solutions of a System of Linear Inequalities. USSR Computational Mathematics and Mathematical Physics. 1965, 5(2):228-233.
[189] N.V. Chernikova. Algorithm for discovering the set of all the solutions of a linear programming problem. USSR Computational Mathematics and Mathematical Physics. 1968, 8(6):282-293.
[190] I. M. Bomze, M. Budinich, P. M. Pardalos, M. Pelillo. T\v maximum clique problem. Handbook of Combinatorial Optimization (Supplement Volume A). Kluwer Academic Publishers, 1999, 1-74.
[191] D. F. Shanno, R. L. Weil. 'Linear' Programming with Absolute-Value Functionals. Operations Research. 1971, 19(l):120-124.
[192] G. B. Dantzig, M. N. Thapa. Linear programming 1: introduction. Secaucus, NJ, USA: Springer-Verlag New York, Inc., 1997.
[193] B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, S. K. Rajamani. SYNERGY: a new algorithm for property checking. SIGSOFT FSE'06. ACM Press, 2006, 117-127.
[194] T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre. Lazy abstraction. ACM POPL'02. ACM Press, 2002, 58-70.