基于不变式的程序验证工具的设计与实现
|
摘要
随着计算机科学的高速发展,软件在人们日常生活中扮演着越来越重要的角色,软件程序的正确性验证研究成为学界高度关注的课题。程序的停机性和安全性验证是程序正确性验证中的两个重要内容,本文基于Mathematica和构造程序不变式,设计并实现了程序的停机性和安全性验证工具,主要工作包括以下几个方面:
1.程序不变式自动构造工具的实现。基于Mathematica平台,设计了一个程序不变式自动构造工具。其中,线性不变式的构造采用CILinear,多项式循环不变式的构造采用Aligator。构造的不变式描述了循环程序变量间的关系,为程序正确性验证提供了计算基础。
2.停机性验证。首先在程序循环点插桩循环计数器记录循环次数,然后构造程序不变式集作为最优化问题的约束系统,并以循环计数器是否存在最小值为最优化问题目标,将停机性验证问题转化为最优化问题,基于Mathematica提供的最优化问题求解函数Minimize,有效实现了程序的停机性验证,而且可以生成精确的循环符号化复杂度上界。
3.安全性验证。首先标注出程序的前后置断言,建立安全性验证命题,用构造出的不变式集形成验证条件,将安全性验证问题转化为使用定理证明器验证不变式集是否蕴含安全性逻辑公式的问题,然后基于定理证明器Theorema中的验证工具PCS,有效实现了程序安全性验证工作。
With the rapid development of computer science, software plays an increasingly important role in people's daily life, so the correctness verification of software program got a great deal attention in academic domain. Termination and safety verification are two important parts of program correctness verification, based on Mathematica and generation of invariant, we design and implement a tool for termination and safety verification. The main contributions are summarized as follows:
1. The implementation of automatic program invariants generation. Based on Mathematica, we have designed and implemented a tool for automatic program invariant generation, which constructs the linear invariants using CILinear and constructs the polynomial loop invaraints using Aligator. The constructed invariants describe the relationships among the loop program variables, and provide the computation basis for the program correctness verification.
2. The implementation of termination verification. First we instrument a counter into program loop to record loop times. Then constructed invariant sets as constraint system and whether counter have minimum as objective function, we transform the termination verification problem into an optimization problem, based on the optimization problem-solving function Minimize in Mathematica, we can not only effectively complete the termination verification, but also generate the exact complexity bound of program loops.
3. The implementation of safety verification. First we instrument the assume and statements, establish the propositions for safety verification, construct the verification conditions with the set of invariants, transform the verification of safety into the verification of the validity of the logic formula that the invariants imply the the propositions characterizing safety. Then based on the theorem prover PCS in Theorema, the logical formula can be constructed from a set of invariants implying a formula which specifies the safety property. We can effectively implement the safety verification of program.
1.程序不变式自动构造工具的实现。基于Mathematica平台,设计了一个程序不变式自动构造工具。其中,线性不变式的构造采用CILinear,多项式循环不变式的构造采用Aligator。构造的不变式描述了循环程序变量间的关系,为程序正确性验证提供了计算基础。
2.停机性验证。首先在程序循环点插桩循环计数器记录循环次数,然后构造程序不变式集作为最优化问题的约束系统,并以循环计数器是否存在最小值为最优化问题目标,将停机性验证问题转化为最优化问题,基于Mathematica提供的最优化问题求解函数Minimize,有效实现了程序的停机性验证,而且可以生成精确的循环符号化复杂度上界。
3.安全性验证。首先标注出程序的前后置断言,建立安全性验证命题,用构造出的不变式集形成验证条件,将安全性验证问题转化为使用定理证明器验证不变式集是否蕴含安全性逻辑公式的问题,然后基于定理证明器Theorema中的验证工具PCS,有效实现了程序安全性验证工作。
With the rapid development of computer science, software plays an increasingly important role in people's daily life, so the correctness verification of software program got a great deal attention in academic domain. Termination and safety verification are two important parts of program correctness verification, based on Mathematica and generation of invariant, we design and implement a tool for termination and safety verification. The main contributions are summarized as follows:
1. The implementation of automatic program invariants generation. Based on Mathematica, we have designed and implemented a tool for automatic program invariant generation, which constructs the linear invariants using CILinear and constructs the polynomial loop invaraints using Aligator. The constructed invariants describe the relationships among the loop program variables, and provide the computation basis for the program correctness verification.
2. The implementation of termination verification. First we instrument a counter into program loop to record loop times. Then constructed invariant sets as constraint system and whether counter have minimum as objective function, we transform the termination verification problem into an optimization problem, based on the optimization problem-solving function Minimize in Mathematica, we can not only effectively complete the termination verification, but also generate the exact complexity bound of program loops.
3. The implementation of safety verification. First we instrument the assume and statements, establish the propositions for safety verification, construct the verification conditions with the set of invariants, transform the verification of safety into the verification of the validity of the logic formula that the invariants imply the the propositions characterizing safety. Then based on the theorem prover PCS in Theorema, the logical formula can be constructed from a set of invariants implying a formula which specifies the safety property. We can effectively implement the safety verification of program.
引文
[1]郑人杰.计算机软件测试技术[M].第1版.北京:清华大学出版社,1992: 1-33.
[2] R. W. Floyd. Assigning meanings to programs [C]. Proc. of a Symposium on Applied Mathematics, NewYork, 1967, Vol. 19: pp. 19-31.
[3] Hoare T. The Verifying Compiler: A Grand Challenge for Computing Research [J]. Journal of the ACM,2003,50(I): 63-69.
[4] WolframResearchInc. Mathematica6.0 [OL]. http://reference.wolfram.com/mathematica/guide/.html, 1999-06-07.
[5] Yang Lu, Zhan Naijun, Xia Bican and Zhou Chaochen. Program Verification by Using DISCOVERER[C]. Position paper in Verified Software: Theories, Tools, Experiments (VSTTE 2005), ETH Zürich. 2005: 10-13.
[6] Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan. Generating Polynomial Invariants with DISCOVERER and QEPCAD [J]. Formal Methods and Hybrid Real-Time Systems 2007: 65-80.
[7] Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, Chaochen Zhou. Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems[C]. ICTAC 2007: 35-48.
[8] Xia Bican and Yang Lu. An algorithm for isolating the real solutions of semi-algebraic systems [J]. J. Symbolic Computation, 2002, 34: 461-477.
[9] Yang Lu. Recent advances on determining the number of real roots of parametric polynomials [J]. J.Symbolic Computation, 1999, 28: 225-242.
[10] Yang Lu and Bican Xia. Real solution classifications of a class of parametric semi-algebraic systems [C]. In Proc.of Int’l Conf. on Algorithmic Algebra and Logi, 2005: 280-290.
[11] Zhisong Tang. A Temporal Logic Language Oriented Toward Software Engineering [J]. Chinese J. of Advanced Software Research, Allerton Press, INC. New York, 1994, 1.
[12]郭亮,唐稚松.基于XYZ/E描述和验证容错系统[J].软件学报,2002:13(5) 913-920.
[13] Jifeng He, Shengchao Qin, Adnan Sherif. Constructing Property-Oriented Models for Verification [C]. UTP 2006: 85-100.
[14] Ji Wang, Xiaodong Yi, Xuejun Yang. Towards a framework for scalable model checking of concurrent C programs [C]. In: Proc. of the IsoLA 2006: 355-362.
[15]易晓东,王戟,杨学军.基于Assume-Guarantee搜索复用的C程序验证方法[J].软件学报,2007, 18(9): 2130-2140.
[16] Rongjie Yan, Guangyuan Li, Zhisong Tang. Symbolic Model Checking of FinitePrecision Timed Automata [C]. ICTAC 2005: 272-287.
[17]武斌.基于符号计算方法的程序验证技术研究[D].上海:华东师范大学软件学院.2010: 1-6.
[18]万松松.循环不变式开发技术研究[D].江西:江西师范大学计算机学院软件与理论专业.2008: 23-28.
[19]何志学.面向对象并发程序切片技术及其在程序验证中的应用[D].江苏:苏州大学计算机学院软件与理论专业.2008:2-8.
[20]文志诚.面向对象软件的形式验证技术[D].上海:上海大学计算机学院控制控制理论与控制工程专业.2007: 1-7.
[21] P. Cousot and R. Cousot. Systematic design of program analysis frameworks [C]. In 6th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages, San Antonio, TX, ACM Press, 1979: 269-282.
[22] P. Cousot. Abstract interpretation based formal methods and future chanllenges[C]. Informatics-10 Years Back, 10 Years Ahead. Springer, LNCS2000: 138-156.
[23] Laurent Mauborgne. ASTRéE: verification of absence of run-time error[C]. In Building the Information Society, R. Jacquard (Ed.), Kluwer Academic Publishers, 2004: 385-392.
[24] P. Cousot and R. Cousot. Abstract Interpretation Based Program Testing [C]. Proceedings of the SSGRR 2000 Computer & eBusiness International Conference. Scuola Superiore G. Reiss Romoli. L'Aquila, Italy, 2000: Compact disk paper 248.
[25] P. Cousot and R. Cousot. Refining Model Checking by Abstract Interpretation [C]. Automated Software Engineering Journal, special issue on Automated Software Analysis, 1999, 6(1): 69-95.
[26] P. Cousot and R. Cousot. Abstract interpretation frameworks [J]. J. Logic and Comp. 1992, 2(4): 511-547.
[27] S. Graf and H. Saidi. Construction of stract state graphs with PVS [C]. In O.Grumberg, Computer-Aided Verification, 1997, LNCS 1254: 72-83.
[28] Michael Colon and Tomas E. Uribe. Generating finite state abstractions of reactive systems using decision procedures [C]. In CAV’98, 1998: 293-304.
[29] S. Das, D. Dill, S.Park. Experience with predicate abstraction [C]. In Halbwachs, Proc. 11th Int. Conf. CAV'99. Trento, IT, Springer-Verlag, LNCS 1633, 1999: 160-171.
[30] S.Chaki, E.Clarke, A.Groce, J.Ouaknine, K.Yorav. Efficient Verification of Sequential and Concurrent C Programs [J]. Formal Methods in System Design, 2005, 25: 129-166.
[31] T. A. Henzinger, R. Jhala, R.Majumdar and S. Qadeer. Thread-modularabstraction refinement [C]. In CAV 2003: Computer Aided Verification, 2003: 262- 274.
[32] S. Qadeer and D. Wu. KISS: Keep it simple and seqeuential [C]. In ACM SIGPLAN Conference on Programming Language Design and Implementation 04: Programming Language Design and Implementation, ACM, 2004: 14-24.
[33] Andreas Podelski, Andrey Rybalchenko. Transition Invariants [C]. In LICS 2004: 32-41.
[34] Andreas Podelski, Andrey Rybalchenko. Transition predicate abstraction and fair termination [C]. ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages 2005: 132-144.
[35] Byron Cook, Andreas Podelski, Andrey Rybalchenko. Abstraction Refinement for Termination [C]. Static Analysis 2005: 87-101.
[36] Byron Cook, Andreas Podelski, Andrey Rybalchenko. Terminator: Beyond Safety [C]. CAV 2006: 415-418.
[37] Byron Cook, Andreas Podelski, Andrey Rybalchenko. Termination proofs for systems code [C]. ACM SIGPLAN Conference on Programming Language Design and Implementation 2006: 415-426.
[38] Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko. Moshe Y. Vardi. Proving that programs eventually do something good [C]. ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages 2007: 265-276.
[39] M. Y. Vardi. Verification of concurrent programs: the automata theoretic framework [J]. Annals of Pure and Applied Logic, 1991, 51: 79-98.
[40] Patrick Cousot. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming [C]. VMCAI 2005: 1-24.
[41]林惠民,张文辉.模型检测:理论、方法与应用[J],电子学报, 2002-12A: 07-12.
[42] Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler and David L. Dill, CMC[C]: A Pragmatic Approach to Model Checking Real Code. OSDI (2002).
[43] Juergen Dingel, Computer-Assisted Assume Guarantee Reasoning with VeriSoft [J]. In proceedings of the 25th International Conference on Software Engineering (ICSE'03) pp. 138-148 (2003).
[44] C. A. R. Hoare. An axiomatic basis of Computer orogramming [J]. Comm. ACM, 1969(12): 576-583.
[45]邢建英.程序验证关键技术研究[D].湖南长沙:国防科学技术大学计算机学院.2011.
[46] Dijkstra E W.A Discipline of Programming [M]. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[47]万松松,薛锦云,谢武平.循环不变式开发技术研究[J],计算机工程与科学,2010,9: 2-3.
[48] Stirewalt K. Dillon L.K.A Component-Based Approach to Building Formal-Analysis Tool[C] . Proc of ICSE’01, 2001: 167-176.
[49] Janota M. Assertion-Based loop Invariant Generation[C] .Proc of the 1st Int’1 Workshop on Invariant Generation,2007.
[50] Fisler K. Krishnamurthi S. Modular Verification of Collabo-ration-Based Software Designs [C].Proc of FSE’01.2001.
[51] B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa,F. Piroi, N. Popov, J. Robu, M. Rosenkranz, and W. Windsteiger. Theorema: Towards Computer-Aided Mathematical Theory Exploration [J]. Journal ofApplied Logic, 2006, 4(4): 470-504.
[52] Ga?l Lalire, Mathias Argoud, and Bertrand Jeannet. Interproc [OL], http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html, 2008.
[53] Patrick Cousot, Radhia Cousot. Static determination of dynamic properties of programs[C]. In: Robinet B, ed. Proc. of the 2nd Int’l Symp. On Programming. Paris, 1976:106-130.
[54] Antoine Mine: The octagon abstract domain [J]. Higher-Order and Symbolic Computation, 2006, 19(1): 31-100.
[55] Patrick Cousot, Nicolas Halbwachs: Automatic Discovery of Linear Restraints among Variables of a Program [C]. ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages 1978: 84-96.
[56]邢建英,李梦君,李舟军.CILinear:一个线性不变式自动构造工具[J]. NCTCS2010,计算机科学,2010,37(12): 91-95.
[57] G. C. Necula, S. McPeak, S. P. Rahul, etal. CIL: Infrastructure for C Program Analysis and Transformation. http://manju.cs.berkeley.edu/cil/, 2007.
[58] G. C. Necula, S. McPeak, S. P. Rahul, etal. CIL: Intermediate Language and Tools for Analysis and Transformation of C programs [C]. Proceedings of Conference on Compiler Construction, 2002: 213-228.
[59] David Wheeler. Flawfinder [OL]. http://www.dwheeler.com/flawfinder/. 2008.
[60] B. Jeannet, A. Miné. APRON: A Library of Numerical Abstract Domains for Static Analysis [C]. In Computer Aided Verification, CAV'2009, 2009, LNCS 5643: 661-667.
[61] Fixpoint [OL]. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/fixpoint /index.html, 2009.
[62] Fran?ois Bourdoncle. Efficient Chaotic Iteration Strategies with Widenings [C]. Proc. of the International Conference on Formal Methods in Programming andtheir Applications, Springer-Verlag, 1993, LNCS735: 128-141.
[63] Laura Kovács. Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema [D]. Doctoral Thesis, RISC, Johannes Kepler University Linz, Austria, 2007.
[64] Tiwari, A. Termination of linear programs [J]. In CAV 2004, LNCS, vol.3114, pp.70-82.
[65] Collins, G. E. Quantifier elimination for real closed fields by cylindrical algebraic decomposition [C]. In GI Conf. Automata Theory and Formal Languages, 1975, 12: 515-532.
[2] R. W. Floyd. Assigning meanings to programs [C]. Proc. of a Symposium on Applied Mathematics, NewYork, 1967, Vol. 19: pp. 19-31.
[3] Hoare T. The Verifying Compiler: A Grand Challenge for Computing Research [J]. Journal of the ACM,2003,50(I): 63-69.
[4] WolframResearchInc. Mathematica6.0 [OL]. http://reference.wolfram.com/mathematica/guide/.html, 1999-06-07.
[5] Yang Lu, Zhan Naijun, Xia Bican and Zhou Chaochen. Program Verification by Using DISCOVERER[C]. Position paper in Verified Software: Theories, Tools, Experiments (VSTTE 2005), ETH Zürich. 2005: 10-13.
[6] Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan. Generating Polynomial Invariants with DISCOVERER and QEPCAD [J]. Formal Methods and Hybrid Real-Time Systems 2007: 65-80.
[7] Yinghua Chen, Bican Xia, Lu Yang, Naijun Zhan, Chaochen Zhou. Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems[C]. ICTAC 2007: 35-48.
[8] Xia Bican and Yang Lu. An algorithm for isolating the real solutions of semi-algebraic systems [J]. J. Symbolic Computation, 2002, 34: 461-477.
[9] Yang Lu. Recent advances on determining the number of real roots of parametric polynomials [J]. J.Symbolic Computation, 1999, 28: 225-242.
[10] Yang Lu and Bican Xia. Real solution classifications of a class of parametric semi-algebraic systems [C]. In Proc.of Int’l Conf. on Algorithmic Algebra and Logi, 2005: 280-290.
[11] Zhisong Tang. A Temporal Logic Language Oriented Toward Software Engineering [J]. Chinese J. of Advanced Software Research, Allerton Press, INC. New York, 1994, 1.
[12]郭亮,唐稚松.基于XYZ/E描述和验证容错系统[J].软件学报,2002:13(5) 913-920.
[13] Jifeng He, Shengchao Qin, Adnan Sherif. Constructing Property-Oriented Models for Verification [C]. UTP 2006: 85-100.
[14] Ji Wang, Xiaodong Yi, Xuejun Yang. Towards a framework for scalable model checking of concurrent C programs [C]. In: Proc. of the IsoLA 2006: 355-362.
[15]易晓东,王戟,杨学军.基于Assume-Guarantee搜索复用的C程序验证方法[J].软件学报,2007, 18(9): 2130-2140.
[16] Rongjie Yan, Guangyuan Li, Zhisong Tang. Symbolic Model Checking of FinitePrecision Timed Automata [C]. ICTAC 2005: 272-287.
[17]武斌.基于符号计算方法的程序验证技术研究[D].上海:华东师范大学软件学院.2010: 1-6.
[18]万松松.循环不变式开发技术研究[D].江西:江西师范大学计算机学院软件与理论专业.2008: 23-28.
[19]何志学.面向对象并发程序切片技术及其在程序验证中的应用[D].江苏:苏州大学计算机学院软件与理论专业.2008:2-8.
[20]文志诚.面向对象软件的形式验证技术[D].上海:上海大学计算机学院控制控制理论与控制工程专业.2007: 1-7.
[21] P. Cousot and R. Cousot. Systematic design of program analysis frameworks [C]. In 6th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages, San Antonio, TX, ACM Press, 1979: 269-282.
[22] P. Cousot. Abstract interpretation based formal methods and future chanllenges[C]. Informatics-10 Years Back, 10 Years Ahead. Springer, LNCS2000: 138-156.
[23] Laurent Mauborgne. ASTRéE: verification of absence of run-time error[C]. In Building the Information Society, R. Jacquard (Ed.), Kluwer Academic Publishers, 2004: 385-392.
[24] P. Cousot and R. Cousot. Abstract Interpretation Based Program Testing [C]. Proceedings of the SSGRR 2000 Computer & eBusiness International Conference. Scuola Superiore G. Reiss Romoli. L'Aquila, Italy, 2000: Compact disk paper 248.
[25] P. Cousot and R. Cousot. Refining Model Checking by Abstract Interpretation [C]. Automated Software Engineering Journal, special issue on Automated Software Analysis, 1999, 6(1): 69-95.
[26] P. Cousot and R. Cousot. Abstract interpretation frameworks [J]. J. Logic and Comp. 1992, 2(4): 511-547.
[27] S. Graf and H. Saidi. Construction of stract state graphs with PVS [C]. In O.Grumberg, Computer-Aided Verification, 1997, LNCS 1254: 72-83.
[28] Michael Colon and Tomas E. Uribe. Generating finite state abstractions of reactive systems using decision procedures [C]. In CAV’98, 1998: 293-304.
[29] S. Das, D. Dill, S.Park. Experience with predicate abstraction [C]. In Halbwachs, Proc. 11th Int. Conf. CAV'99. Trento, IT, Springer-Verlag, LNCS 1633, 1999: 160-171.
[30] S.Chaki, E.Clarke, A.Groce, J.Ouaknine, K.Yorav. Efficient Verification of Sequential and Concurrent C Programs [J]. Formal Methods in System Design, 2005, 25: 129-166.
[31] T. A. Henzinger, R. Jhala, R.Majumdar and S. Qadeer. Thread-modularabstraction refinement [C]. In CAV 2003: Computer Aided Verification, 2003: 262- 274.
[32] S. Qadeer and D. Wu. KISS: Keep it simple and seqeuential [C]. In ACM SIGPLAN Conference on Programming Language Design and Implementation 04: Programming Language Design and Implementation, ACM, 2004: 14-24.
[33] Andreas Podelski, Andrey Rybalchenko. Transition Invariants [C]. In LICS 2004: 32-41.
[34] Andreas Podelski, Andrey Rybalchenko. Transition predicate abstraction and fair termination [C]. ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages 2005: 132-144.
[35] Byron Cook, Andreas Podelski, Andrey Rybalchenko. Abstraction Refinement for Termination [C]. Static Analysis 2005: 87-101.
[36] Byron Cook, Andreas Podelski, Andrey Rybalchenko. Terminator: Beyond Safety [C]. CAV 2006: 415-418.
[37] Byron Cook, Andreas Podelski, Andrey Rybalchenko. Termination proofs for systems code [C]. ACM SIGPLAN Conference on Programming Language Design and Implementation 2006: 415-426.
[38] Byron Cook, Alexey Gotsman, Andreas Podelski, Andrey Rybalchenko. Moshe Y. Vardi. Proving that programs eventually do something good [C]. ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages 2007: 265-276.
[39] M. Y. Vardi. Verification of concurrent programs: the automata theoretic framework [J]. Annals of Pure and Applied Logic, 1991, 51: 79-98.
[40] Patrick Cousot. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming [C]. VMCAI 2005: 1-24.
[41]林惠民,张文辉.模型检测:理论、方法与应用[J],电子学报, 2002-12A: 07-12.
[42] Madanlal Musuvathi, David Y. W. Park, Andy Chou, Dawson R. Engler and David L. Dill, CMC[C]: A Pragmatic Approach to Model Checking Real Code. OSDI (2002).
[43] Juergen Dingel, Computer-Assisted Assume Guarantee Reasoning with VeriSoft [J]. In proceedings of the 25th International Conference on Software Engineering (ICSE'03) pp. 138-148 (2003).
[44] C. A. R. Hoare. An axiomatic basis of Computer orogramming [J]. Comm. ACM, 1969(12): 576-583.
[45]邢建英.程序验证关键技术研究[D].湖南长沙:国防科学技术大学计算机学院.2011.
[46] Dijkstra E W.A Discipline of Programming [M]. Englewood Cliffs, NJ: Prentice-Hall, 1976.
[47]万松松,薛锦云,谢武平.循环不变式开发技术研究[J],计算机工程与科学,2010,9: 2-3.
[48] Stirewalt K. Dillon L.K.A Component-Based Approach to Building Formal-Analysis Tool[C] . Proc of ICSE’01, 2001: 167-176.
[49] Janota M. Assertion-Based loop Invariant Generation[C] .Proc of the 1st Int’1 Workshop on Invariant Generation,2007.
[50] Fisler K. Krishnamurthi S. Modular Verification of Collabo-ration-Based Software Designs [C].Proc of FSE’01.2001.
[51] B. Buchberger, A. Craciun, T. Jebelean, L. Kovacs, T. Kutsia, K. Nakagawa,F. Piroi, N. Popov, J. Robu, M. Rosenkranz, and W. Windsteiger. Theorema: Towards Computer-Aided Mathematical Theory Exploration [J]. Journal ofApplied Logic, 2006, 4(4): 470-504.
[52] Ga?l Lalire, Mathias Argoud, and Bertrand Jeannet. Interproc [OL], http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html, 2008.
[53] Patrick Cousot, Radhia Cousot. Static determination of dynamic properties of programs[C]. In: Robinet B, ed. Proc. of the 2nd Int’l Symp. On Programming. Paris, 1976:106-130.
[54] Antoine Mine: The octagon abstract domain [J]. Higher-Order and Symbolic Computation, 2006, 19(1): 31-100.
[55] Patrick Cousot, Nicolas Halbwachs: Automatic Discovery of Linear Restraints among Variables of a Program [C]. ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages 1978: 84-96.
[56]邢建英,李梦君,李舟军.CILinear:一个线性不变式自动构造工具[J]. NCTCS2010,计算机科学,2010,37(12): 91-95.
[57] G. C. Necula, S. McPeak, S. P. Rahul, etal. CIL: Infrastructure for C Program Analysis and Transformation. http://manju.cs.berkeley.edu/cil/, 2007.
[58] G. C. Necula, S. McPeak, S. P. Rahul, etal. CIL: Intermediate Language and Tools for Analysis and Transformation of C programs [C]. Proceedings of Conference on Compiler Construction, 2002: 213-228.
[59] David Wheeler. Flawfinder [OL]. http://www.dwheeler.com/flawfinder/. 2008.
[60] B. Jeannet, A. Miné. APRON: A Library of Numerical Abstract Domains for Static Analysis [C]. In Computer Aided Verification, CAV'2009, 2009, LNCS 5643: 661-667.
[61] Fixpoint [OL]. http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/fixpoint /index.html, 2009.
[62] Fran?ois Bourdoncle. Efficient Chaotic Iteration Strategies with Widenings [C]. Proc. of the International Conference on Formal Methods in Programming andtheir Applications, Springer-Verlag, 1993, LNCS735: 128-141.
[63] Laura Kovács. Automated Invariant Generation by Algebraic Techniques for Imperative Program Verification in Theorema [D]. Doctoral Thesis, RISC, Johannes Kepler University Linz, Austria, 2007.
[64] Tiwari, A. Termination of linear programs [J]. In CAV 2004, LNCS, vol.3114, pp.70-82.
[65] Collins, G. E. Quantifier elimination for real closed fields by cylindrical algebraic decomposition [C]. In GI Conf. Automata Theory and Formal Languages, 1975, 12: 515-532.