循环不变式生成方法研究与改进
摘要
软件作为信息系统的实现载体,广泛应用在各个领域,软件中的任何安全漏洞或错误的实现都可能导致非常严重的后果。通过大量的测试可以提高软件的可靠性,但成本较高,也不能完全保证软件的可靠。形式化证明方法基于严密的数学和逻辑基础,经过正确性证明的程序可以保证软件符合指定的程序规范,从而大大提高软件可靠性。
程序正确性证明的一个关键问题是发现充分的循环不变式信息来辅助、支撑证明过程的完成。由人工寻找循环不变式工作繁琐,容易出错。因此,研究如何自动地有效分析和生成循环不变式,使得软件证明过程顺利完成,成为形式化方法研究领域的一个重要研究课题。本文主要针对软件验证技术中的循环不变式生成技术进行研究和实现：
(1)对形式化程序分析方法主要理论进行总结。本文根据形式化分析中用到的主要理论的不同对形式化分析技术进行总结。对各自的理论核心、主要解决的问题、典型工具进行了阐述。在此基础上,指出形式化证明过程的难点,并总结了当前克服这些难点所采用的方法。
(2)介绍和总结了目前求解循环不变式的主要研究状况和现有方法。根据他们主要理论和适用范围的不同进行阐述,指出了目前工作存在的不足。
(3)本文提出了一种基于条件赋值转换和自适应模板技术的循环不变式生成方法。根据程序控制流结构、依赖分析结果和值分析结果,生成可能的循环不变式,然后由定理证明器求解。该方法可以自动地运行,并将结果以ACSL注释的形式添加到程序中,辅助完成程序属性的证明过程。
(4)基于上述方法,在Frama-C平台和APRON库的基础上,实现了一个分析插件loopInv。选取了一些程序作为分析对象,与其他方法作了比较,结果表明可以发现更多的不变式,使一些程序规范顺利得到证明。
Software has been used widely in various areas as the carrier of information systems. Any vulnerability or incorrect development in software will cause highly serious failures. It can increase the confidence with enough testing which will be very expensive. Unfortunately, it still cannot guarantee that the software to be tested is fully reliability even with lots of testing. Formal methods are based on strict mathematically and logically basis. It can ensure that the software meets its given specifications through proving of correctness, which greatly improves the reliability of software.
A key issue in program proving is finding sufficient loop invariants to assist the automatic process. However, writing loop invariants manually is boring and error-prone. Thus, the research on how to analysis and generate loop invariants automatically becomes an important issue in the area of formal methods. This dissertation focused on the generation of loop invariants and mainly covers the subjects of theory of formal methods and generation technologies for invariants.
(1)We summarized the main theories of formal methods to analysis programs. It is focused on the core theory, the main problem to resolve and classical tools. Then we point out the difficulty of formal proof.
(2) We summarized recent research and common technologies for generating loop invariants. They are described and compared from many aspects, including the kinds of programs to be analyzed, the way how they work and their shortcomings.
(3) Based on conditional assignment and adaptive template an approach to generate invariants is proposed in this dissertation. Many semantic factors are considiered here, not only loop itself but also specifications, asserts etc.. It infers potential loop invariants according to CFG, PDG and value analysis which are then resolved by theory prover. It can run automatically and insert invariants as ACSL comments into C codes as output.
(4)Based on the method above, a plugin named looplnv is designed and implemented with the platform Frama-C and APRON. According to the experiments on some selected programs, it can generate more invariants comparing with other tools and most of the programs can be proved successfully.
程序正确性证明的一个关键问题是发现充分的循环不变式信息来辅助、支撑证明过程的完成。由人工寻找循环不变式工作繁琐,容易出错。因此,研究如何自动地有效分析和生成循环不变式,使得软件证明过程顺利完成,成为形式化方法研究领域的一个重要研究课题。本文主要针对软件验证技术中的循环不变式生成技术进行研究和实现：
(1)对形式化程序分析方法主要理论进行总结。本文根据形式化分析中用到的主要理论的不同对形式化分析技术进行总结。对各自的理论核心、主要解决的问题、典型工具进行了阐述。在此基础上,指出形式化证明过程的难点,并总结了当前克服这些难点所采用的方法。
(2)介绍和总结了目前求解循环不变式的主要研究状况和现有方法。根据他们主要理论和适用范围的不同进行阐述,指出了目前工作存在的不足。
(3)本文提出了一种基于条件赋值转换和自适应模板技术的循环不变式生成方法。根据程序控制流结构、依赖分析结果和值分析结果,生成可能的循环不变式,然后由定理证明器求解。该方法可以自动地运行,并将结果以ACSL注释的形式添加到程序中,辅助完成程序属性的证明过程。
(4)基于上述方法,在Frama-C平台和APRON库的基础上,实现了一个分析插件loopInv。选取了一些程序作为分析对象,与其他方法作了比较,结果表明可以发现更多的不变式,使一些程序规范顺利得到证明。
Software has been used widely in various areas as the carrier of information systems. Any vulnerability or incorrect development in software will cause highly serious failures. It can increase the confidence with enough testing which will be very expensive. Unfortunately, it still cannot guarantee that the software to be tested is fully reliability even with lots of testing. Formal methods are based on strict mathematically and logically basis. It can ensure that the software meets its given specifications through proving of correctness, which greatly improves the reliability of software.
A key issue in program proving is finding sufficient loop invariants to assist the automatic process. However, writing loop invariants manually is boring and error-prone. Thus, the research on how to analysis and generate loop invariants automatically becomes an important issue in the area of formal methods. This dissertation focused on the generation of loop invariants and mainly covers the subjects of theory of formal methods and generation technologies for invariants.
(1)We summarized the main theories of formal methods to analysis programs. It is focused on the core theory, the main problem to resolve and classical tools. Then we point out the difficulty of formal proof.
(2) We summarized recent research and common technologies for generating loop invariants. They are described and compared from many aspects, including the kinds of programs to be analyzed, the way how they work and their shortcomings.
(3) Based on conditional assignment and adaptive template an approach to generate invariants is proposed in this dissertation. Many semantic factors are considiered here, not only loop itself but also specifications, asserts etc.. It infers potential loop invariants according to CFG, PDG and value analysis which are then resolved by theory prover. It can run automatically and insert invariants as ACSL comments into C codes as output.
(4)Based on the method above, a plugin named looplnv is designed and implemented with the platform Frama-C and APRON. According to the experiments on some selected programs, it can generate more invariants comparing with other tools and most of the programs can be proved successfully.
引文
[Ball01]Ball T, Majumdar R, Millstein TD, Rajamani SK. Automatic Predicate Abstraction of C Programs. In Proceedings of PLDI.2001:203-213.
[Ball02]Ball T, Rajamani SK. The SLAM project:debugging system software via static analysis. In Proceedings of POPL.2002:1-3.
[Ball04]Ball T, Cook B, Levin V, Rajamani SK. SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In Proceedings of IFM. 2004:1-20.
[Barrett07] Barrett C, Tinelli C. In Proceedings of CAV.2007:298-302.
[Baudin08]Baudin P, Cuoq P, Filliatre JC, Marche C,Monate B, Moy Y, Prevosto V. ACSL:ANSI/ISO C Specification Language.from http://frama-c.cea.fr/acsl.html. 2008.
[Beyer07]Beyer D, Henzinger TA, Jhala R, Majumdar R. The software model checker Blast. In Proceedings of STTT.2007:505-525.
[Blanchet02] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Mine A, Monniaux D, Rival X. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In Proceedings of The Essence of Computation.2002:85-108.
[Blanchet03] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Mine A, Monniaux D, Rival X. A static analyzer for large safety-critical software. In Proceedings of PLDI.2003:196-207.
[Bourdoncle93] Bourdoncle F. Efficient chaotic iteration strategies with widenings. In Proceedings of FMP&TA.1993:128-141.
[Bradley05] Bradley AR, Manna Z, Sipma HB. Linear ranking with reachability. In Proceedings of CAV.2005:491-504.
[Bradley08] Bradley AR, Manna Z. Property-Directed Incremental Invariant Generation. In Proceedings of Formal Asp. Comput..2008:379-405.
[Bush00]Bush WR, Pincus JD, Sielaff DJ. A static analyzer for finding dynamic programming errors. In Proceedings of Softw., Pract. Exper..2000:775-802.
[Chaki03a]Chaki S, Clarke EM, Groce A, Jha S, Veith H. Modular Verification of Software Components in C. In Proceedings of ICSE.2003:385-395.
[Chaki03b]Chaki S, Clarke EM, Groce A, Strichman O. Predicate Abstraction with Minimum Predicates. In Proceedings of CHARME.2003:19-34.
[Chen 04]Chen H, Dean D, Wagner D. Model Checking One Million Lines of C Code. In Proceedings of NDSS.2004:171-185.
[Chen08]Chen LJ, Mine A, Cousot P. A sound floating-point polyhedra abstract domain. In Proceedings of APLAS.2008:3-18.
[Chen02]Chen H, Wagner D. MOPS an infrastructure for examining security properties of software. In Proceedings of CCS.2002:235-244.
[Cimatti02] Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2:An OpenSource Tool for Symbolic Model Checking. In Proceedings of CAV.2002:359-364.
[Cimatti99] Cimatti A, Clarke EM, Giunchiglia F, Roveri M. NuSMV:A New Symbolic Model Verifier. In Proceedings of CAV.1999:495-499.
[Clariso04] Clariso R, Cortadella J. The octahedron abstract domain. In Proceedings of SAS. 2004:312-327.
[Clarke81]Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of 25 Years of Model Checking.2008:196-215.
[Clarke00a] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided Abstraction Refinement. In Proceedings of CAV.2000:154-169.
[Clarke00b] Clarke EM, Grumberg O, Peled DA. Model Checking, The MIT Press.2000.
[Colon03]Colon M, Sankaranarayanan S, Sipma H. Linear invariant generation using non-linear constraint solving. In Proceedings of CAV.2003:420-432.
[Conchon08] Conchon S, Contejean E. The Alt-Ergo automatic theorem prover. from http://alt-ergo.lri.fr/.2008.
[Cousot77]Cousot P, Cousot R. Abstract Interpretation:A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of POPL.1977:238-252.
[Cousot78]Cousot P, Halbwachs N. Automatic Discovery of Linear Restraints Among Variables of a Program. In Proceedings of POPL.1978:84-96.
[Cousot79]Cousot P, Cousot R. Systematic Design of Program Analysis Frameworks. In Proceedings of POPL.1979:269-282.
[Cousot01]Cousot P. Abstract Interpretation Based Formal Methods and Future Challenges. In Proceedings of Informatics.2001:138-156.
[Cousot11]Cousot P, Cousot R, Logozzo F. A parametric segmentation functor for fully automatic and scalable array content analysis. In Proceedings of POPL.2011: 105-118.
[Das03]Das S. PREDICATE ABSTRACTION. Department of Electrical Engineering, Stanford University. PhD thesis.2003:103.
[Das02]Das M, Lerner S, Seigle M. ESP:path-sensitive program verification in polynomial time. In Proceedings of PLDI.2002:57-68.
[Detlefs05] Detlefs D, Nelson G, Saxe JB. Simplify:a theorem prover for program checking. In Proceedings of J. ACM.2005:365-473.
[Ernst07]Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C. The Daikon system for dynamic detection of likely invariants. In Proceedings of Sci. Comput. Program..2007:35-45.
[Flanagan02] Flanagan C, Qadeer S. Predicate Abstraction for Software Verification. In Proceedings of POPL.2002:191-202.
[FLOYD67]FLOYD RW. Assigning Meaning to Programs. In Proceedings of Amer. Math. Soc. Symposia in Applied Mathematics.1967,19:19-31.
[Furia10]Furia CA, Meyer B. Inferring Loop Invariants Using Postconditions, In Proceedings of Fields of Logic and Computation.2010:277-300.
[Gopan05]Gopan D, Reps TW, Sagiv S. A framework for numeric analysis of array operations. In Proceedings of POPL.2005:338-350.
[Gopan06]Gopan D, Reps TW. Lookahead widening. In Proceedings of CAV.2006: 452-466.
[Gopan07a]Gopan D. Numeric program analysis techniques with applications to array analysis and library summarization, The University of Wisconsin. PhD thesis. 2007:231.
[Gopan07b]Gopan D, Reps TW. Guided Static Analysis. In Proceedings of SAS.2007: 349-365.
[Graf97]Graf S, Saidi H. Construction of abstract state graphs with PVS. In Proceedings of CAV.1997:72-83.
[Gulavani08] Gulavani BS, Chakraborty S, Nori AV, Rajamani SK. Automatically refining abstract interpretations. In Proceedings of TACAS.2008:443-458.
[Gulwani09a] Gulwani S, Jain S, Koskinen E. Control-flow refinement and progress invariants for bound analysis. In Proceedings of PLDI.2009:375-385.
[Gulwani09b] Gulwani S, Juvekar S. Bound analysis using backward symbolic execution. Technical report.2009:10.
[Gulwani08] Gulwani S, Srivastava S, Venkatesan R. Program analysis as constraint solving. In Proceedings of PLDI.2008:281-292.
[Gulwani10] Gulwani S, Zuleger F. The reachability-bound problem. In Proceedings of PLDI. 2010:292-304.
[Gupta09]Gupta A, Rybalchenko A. InvGen:An Efficient Invariant Generator. In Proceedings of CAV.2009:634-640.
[Halbwachs08] Halbwachs N, Peron M. Discovering properties about arrays in simple programs. In Proceedings of PLDI.2008:339-348.
[Hart08]Hart TE, Ku K, Gurfinkel A, Chechik M, Lie D. PtYasm:Software Model Checking with Proof Templates. In Proceedings of ASE.2008:479-480.
[Hatcliff01] Hatcliff J, Dwyer MB. Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software. In Proceedings of CONCUR.2001:39-58.
[Havelund00] Havelund K, Pressburger T. Model Checking JAVA Programs using JAVA PathFinder. In Proceedings of STTT.2000:366-381.
[Henzinger02] Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In Proceedings of POPL.2002:58-70.
[Henzinger03] Henzinger TA, Jhala R, Majumdar R, Sutre G. Software verification with BLAST. Software Verification with BLAST. In Proceedings of SPIN.2003:235-239.
[Holzmann97] Holzmann GJ. The Model Checker SPIN. In Proceedings of IEEE Trans. Software Eng..1997:279-295.
[INRIA11]INRIA. The Caml Language. from http://caml.inria.fr/.2011.
[Jeannet09] Jeannet B, Mine A. Apron:A Library of Numerical Abstract Domains for Static Analysis. In Proceedings of CAV.2009:661-667.
[Jhala09]Jhala R, Majumdar R. Software model checking. In Proceedings of ACM Comput. Surv..2009:54.
[Jung10]Jung Y, Kong S, Wang B, Yi K. Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction. In Proceedings of VMCAI.2010: 180-196.
[Jungl1]Jung Y, Kong S, David C, Wang BY, Yi K. Automatically Inferring Loop Invariants via Algorithmic Learning. In Proceedings of Mathematical Structures in Computer Science.2011:25.
[Kapur04]Kapur D. Automatically Generating Loop Invariants Using Quantifier Elimination. In Proceedings of Deduction and Applications.2005:17.
[Kiezun09]Kiezun A, Ganesh V, Guo PJ, Hooimeijer P, Ernst MD. HAMPI:a solver for string constraints. In Proceedings of ISSTA.2009:105-116.
[Kildal173] Kildall GA. A Unified Approach to Global Program Optimization. In Proceedings of POPL.1973:194-206.
[King76]King JC. Symbolic Execution and Program Testing. In Proceedings of Commun. ACM.1976:385-394.
[Kovacs09]Kovacs L, Voronkov A. Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In Proceedings of FASE.2009:470-485.
[Lahiri04]Lahiri SK, Bryant RE. Indexed Predicate Discovery for Unbounded System Verification. In Proceedings of CAV.2004:135-147.
[Lalire]Lalire G, Argoud M, Jeannet B. Interproc. from http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html.
[Mac an Airchinnigh 93] Mac an Airchinnigh M. Formal Methods & Testing. In Tutorials of the Sixth International Software Quality Week. Software Research Institute.1993.
[Manna95]Manna Z, Pnueli A. Temporal verification of reactive systems-safety.1995: 1-512.
[Mauborgne04] Mauborgne L. Astree:verification of absence of run-time error. In Proceedings of IFIP Congress Topical Sessions.2004:385-392.
[Mine06]Mine A. The octagon abstract domain. In Proceedings of Higher-Order and Symbolic Computation.2006:31-100.
[Mine07]Mine A. The Apron Library. CEA Seminar.2007.
[Monate08]Monate B, Signoles J. Slicing for Security of Code. In Proceedings of TRUST. 2008:133-142.
[Monniaux08] Monniaux D. A Quantifier Elimination Algorithm for Linear Real Arithmetic. In Proceedings of LPAR.2008:243-257.
[Moura08]Moura LMD, Bjorner N. Z3:An Efficient SMT Solver. In Proceedings of TACAS.2008:337-340.
[Moy09]Moy Y. Automatic Modular Static Safety Checking for C Programs. Universite Paris-Sud. PhD thesis.2009:249.
[Moyl 0]Moy Y, Marche C. Modular inference of subprogram contracts for safety checking. In Proceedings of J. Symb. Comput.2010:1184-1211.
[Necula02]Necula GC, McPeak S, Rahul SP, Weimer W. CIL:Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proceedings of CC. 2002:213-228.
[Necula09]Necula G, McPeak S, Weimer W, Liblit B, Harren M. CIL:Infrastructure for C Program Analysis and Transformation.from http://www.cs.berkeley.edu/-necula/cil/CIL.pdf.2009.
[Podelski04] Podelski A, Rybalchenko A. A Complete Method for the Synthesis of Linear Ranking Functions. In Proceedings of VMCAI.2004:239-251.
[Queille82] Queille J, Sifakis J. Specification and verification of concurrent systems in CESAR. In Proceedings of Symposium on Programming.1982:337-351.
[Riazanov02] Riazanov A, Voronkov A. The design and implementation of VAMPIRE. In Proceedings of Al Commun..2002:91-110.
[Sankaranarayanan04] Sankaranarayanan S, Sipma H, Manna Z. Non-linear loop invariant generation using Grobner bases. In Proceedings of POPL.2004:318-329.
[Schmitt07] Schmitt PH, Weiβ B. Inferring Invariants by Symbolic Execution. In Proceedings of VERIFY.2007:195-210.
[Schwarz05] Schwarz B, Chen H, Wagner D, Lin J, Tu W, Morrison G, West J. Model Checking An Entire Linux Distribution for Security Violations. In Proceedings of ACSAC.2005:13-22.
[Sharmal1]Sharma R, Dillig I, Dillig T, Aiken A. Simplifying Loop Invariant Generation Using Splitter Predicates. In Proceedings of CAV.2011:703-719.
[Simon03]Simon A, King A, Howe JM. Two Variables per Linear Inequality as an Abstract Domain. In Proceedings of LOPSTR.2002:71-89.
[Wang07]Wang C, Yang Z, Gupta A, Ivancic F. Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. In Proceedings of CAV. 2007:352-365.
[Wei11]Wei Y, Furia CA, Kazmin N, Meyer B. Inferring better contracts. In Proceedings of ICSE.2011:191-200.
[Weiser81]Weiser M. Program slicing. In Proceedings of ICSE.1981:439-449.
[Zitser04]Zitser M, Lippmann R, Leek T. Testing static analysis tools using exploitable buffer overflows from open source code. In Proceedings of SIGSOFT FSE.2004: 97-106.
[屈婉霞08]屈婉霞,李暾,郭阳,杨晓东.谓词抽象技术研究.软件学报.2008,19(1)：27-38.
[王燕妮10]王燕妮.基于不变式的软件故障检测与恢复技术研究.国防科学技术大学,硕士学位论文.2010：71.
[邢建英10]邢建英,李梦君,李舟军.CILinear:一个线性不变式自动构造工具.计算机科学.2010,37(12)：91-95.
[Ball02]Ball T, Rajamani SK. The SLAM project:debugging system software via static analysis. In Proceedings of POPL.2002:1-3.
[Ball04]Ball T, Cook B, Levin V, Rajamani SK. SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In Proceedings of IFM. 2004:1-20.
[Barrett07] Barrett C, Tinelli C. In Proceedings of CAV.2007:298-302.
[Baudin08]Baudin P, Cuoq P, Filliatre JC, Marche C,Monate B, Moy Y, Prevosto V. ACSL:ANSI/ISO C Specification Language.from http://frama-c.cea.fr/acsl.html. 2008.
[Beyer07]Beyer D, Henzinger TA, Jhala R, Majumdar R. The software model checker Blast. In Proceedings of STTT.2007:505-525.
[Blanchet02] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Mine A, Monniaux D, Rival X. Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software. In Proceedings of The Essence of Computation.2002:85-108.
[Blanchet03] Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Mine A, Monniaux D, Rival X. A static analyzer for large safety-critical software. In Proceedings of PLDI.2003:196-207.
[Bourdoncle93] Bourdoncle F. Efficient chaotic iteration strategies with widenings. In Proceedings of FMP&TA.1993:128-141.
[Bradley05] Bradley AR, Manna Z, Sipma HB. Linear ranking with reachability. In Proceedings of CAV.2005:491-504.
[Bradley08] Bradley AR, Manna Z. Property-Directed Incremental Invariant Generation. In Proceedings of Formal Asp. Comput..2008:379-405.
[Bush00]Bush WR, Pincus JD, Sielaff DJ. A static analyzer for finding dynamic programming errors. In Proceedings of Softw., Pract. Exper..2000:775-802.
[Chaki03a]Chaki S, Clarke EM, Groce A, Jha S, Veith H. Modular Verification of Software Components in C. In Proceedings of ICSE.2003:385-395.
[Chaki03b]Chaki S, Clarke EM, Groce A, Strichman O. Predicate Abstraction with Minimum Predicates. In Proceedings of CHARME.2003:19-34.
[Chen 04]Chen H, Dean D, Wagner D. Model Checking One Million Lines of C Code. In Proceedings of NDSS.2004:171-185.
[Chen08]Chen LJ, Mine A, Cousot P. A sound floating-point polyhedra abstract domain. In Proceedings of APLAS.2008:3-18.
[Chen02]Chen H, Wagner D. MOPS an infrastructure for examining security properties of software. In Proceedings of CCS.2002:235-244.
[Cimatti02] Cimatti A, Clarke EM, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2:An OpenSource Tool for Symbolic Model Checking. In Proceedings of CAV.2002:359-364.
[Cimatti99] Cimatti A, Clarke EM, Giunchiglia F, Roveri M. NuSMV:A New Symbolic Model Verifier. In Proceedings of CAV.1999:495-499.
[Clariso04] Clariso R, Cortadella J. The octahedron abstract domain. In Proceedings of SAS. 2004:312-327.
[Clarke81]Clarke EM, Emerson EA. Design and synthesis of synchronization skeletons using branching time temporal logic. In Proceedings of 25 Years of Model Checking.2008:196-215.
[Clarke00a] Clarke EM, Grumberg O, Jha S, Lu Y, Veith H. Counterexample-Guided Abstraction Refinement. In Proceedings of CAV.2000:154-169.
[Clarke00b] Clarke EM, Grumberg O, Peled DA. Model Checking, The MIT Press.2000.
[Colon03]Colon M, Sankaranarayanan S, Sipma H. Linear invariant generation using non-linear constraint solving. In Proceedings of CAV.2003:420-432.
[Conchon08] Conchon S, Contejean E. The Alt-Ergo automatic theorem prover. from http://alt-ergo.lri.fr/.2008.
[Cousot77]Cousot P, Cousot R. Abstract Interpretation:A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of POPL.1977:238-252.
[Cousot78]Cousot P, Halbwachs N. Automatic Discovery of Linear Restraints Among Variables of a Program. In Proceedings of POPL.1978:84-96.
[Cousot79]Cousot P, Cousot R. Systematic Design of Program Analysis Frameworks. In Proceedings of POPL.1979:269-282.
[Cousot01]Cousot P. Abstract Interpretation Based Formal Methods and Future Challenges. In Proceedings of Informatics.2001:138-156.
[Cousot11]Cousot P, Cousot R, Logozzo F. A parametric segmentation functor for fully automatic and scalable array content analysis. In Proceedings of POPL.2011: 105-118.
[Das03]Das S. PREDICATE ABSTRACTION. Department of Electrical Engineering, Stanford University. PhD thesis.2003:103.
[Das02]Das M, Lerner S, Seigle M. ESP:path-sensitive program verification in polynomial time. In Proceedings of PLDI.2002:57-68.
[Detlefs05] Detlefs D, Nelson G, Saxe JB. Simplify:a theorem prover for program checking. In Proceedings of J. ACM.2005:365-473.
[Ernst07]Ernst MD, Perkins JH, Guo PJ, McCamant S, Pacheco C, Tschantz MS, Xiao C. The Daikon system for dynamic detection of likely invariants. In Proceedings of Sci. Comput. Program..2007:35-45.
[Flanagan02] Flanagan C, Qadeer S. Predicate Abstraction for Software Verification. In Proceedings of POPL.2002:191-202.
[FLOYD67]FLOYD RW. Assigning Meaning to Programs. In Proceedings of Amer. Math. Soc. Symposia in Applied Mathematics.1967,19:19-31.
[Furia10]Furia CA, Meyer B. Inferring Loop Invariants Using Postconditions, In Proceedings of Fields of Logic and Computation.2010:277-300.
[Gopan05]Gopan D, Reps TW, Sagiv S. A framework for numeric analysis of array operations. In Proceedings of POPL.2005:338-350.
[Gopan06]Gopan D, Reps TW. Lookahead widening. In Proceedings of CAV.2006: 452-466.
[Gopan07a]Gopan D. Numeric program analysis techniques with applications to array analysis and library summarization, The University of Wisconsin. PhD thesis. 2007:231.
[Gopan07b]Gopan D, Reps TW. Guided Static Analysis. In Proceedings of SAS.2007: 349-365.
[Graf97]Graf S, Saidi H. Construction of abstract state graphs with PVS. In Proceedings of CAV.1997:72-83.
[Gulavani08] Gulavani BS, Chakraborty S, Nori AV, Rajamani SK. Automatically refining abstract interpretations. In Proceedings of TACAS.2008:443-458.
[Gulwani09a] Gulwani S, Jain S, Koskinen E. Control-flow refinement and progress invariants for bound analysis. In Proceedings of PLDI.2009:375-385.
[Gulwani09b] Gulwani S, Juvekar S. Bound analysis using backward symbolic execution. Technical report.2009:10.
[Gulwani08] Gulwani S, Srivastava S, Venkatesan R. Program analysis as constraint solving. In Proceedings of PLDI.2008:281-292.
[Gulwani10] Gulwani S, Zuleger F. The reachability-bound problem. In Proceedings of PLDI. 2010:292-304.
[Gupta09]Gupta A, Rybalchenko A. InvGen:An Efficient Invariant Generator. In Proceedings of CAV.2009:634-640.
[Halbwachs08] Halbwachs N, Peron M. Discovering properties about arrays in simple programs. In Proceedings of PLDI.2008:339-348.
[Hart08]Hart TE, Ku K, Gurfinkel A, Chechik M, Lie D. PtYasm:Software Model Checking with Proof Templates. In Proceedings of ASE.2008:479-480.
[Hatcliff01] Hatcliff J, Dwyer MB. Using the Bandera Tool Set to Model-Check Properties of Concurrent Java Software. In Proceedings of CONCUR.2001:39-58.
[Havelund00] Havelund K, Pressburger T. Model Checking JAVA Programs using JAVA PathFinder. In Proceedings of STTT.2000:366-381.
[Henzinger02] Henzinger TA, Jhala R, Majumdar R, Sutre G. Lazy abstraction. In Proceedings of POPL.2002:58-70.
[Henzinger03] Henzinger TA, Jhala R, Majumdar R, Sutre G. Software verification with BLAST. Software Verification with BLAST. In Proceedings of SPIN.2003:235-239.
[Holzmann97] Holzmann GJ. The Model Checker SPIN. In Proceedings of IEEE Trans. Software Eng..1997:279-295.
[INRIA11]INRIA. The Caml Language. from http://caml.inria.fr/.2011.
[Jeannet09] Jeannet B, Mine A. Apron:A Library of Numerical Abstract Domains for Static Analysis. In Proceedings of CAV.2009:661-667.
[Jhala09]Jhala R, Majumdar R. Software model checking. In Proceedings of ACM Comput. Surv..2009:54.
[Jung10]Jung Y, Kong S, Wang B, Yi K. Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction. In Proceedings of VMCAI.2010: 180-196.
[Jungl1]Jung Y, Kong S, David C, Wang BY, Yi K. Automatically Inferring Loop Invariants via Algorithmic Learning. In Proceedings of Mathematical Structures in Computer Science.2011:25.
[Kapur04]Kapur D. Automatically Generating Loop Invariants Using Quantifier Elimination. In Proceedings of Deduction and Applications.2005:17.
[Kiezun09]Kiezun A, Ganesh V, Guo PJ, Hooimeijer P, Ernst MD. HAMPI:a solver for string constraints. In Proceedings of ISSTA.2009:105-116.
[Kildal173] Kildall GA. A Unified Approach to Global Program Optimization. In Proceedings of POPL.1973:194-206.
[King76]King JC. Symbolic Execution and Program Testing. In Proceedings of Commun. ACM.1976:385-394.
[Kovacs09]Kovacs L, Voronkov A. Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In Proceedings of FASE.2009:470-485.
[Lahiri04]Lahiri SK, Bryant RE. Indexed Predicate Discovery for Unbounded System Verification. In Proceedings of CAV.2004:135-147.
[Lalire]Lalire G, Argoud M, Jeannet B. Interproc. from http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/index.html.
[Mac an Airchinnigh 93] Mac an Airchinnigh M. Formal Methods & Testing. In Tutorials of the Sixth International Software Quality Week. Software Research Institute.1993.
[Manna95]Manna Z, Pnueli A. Temporal verification of reactive systems-safety.1995: 1-512.
[Mauborgne04] Mauborgne L. Astree:verification of absence of run-time error. In Proceedings of IFIP Congress Topical Sessions.2004:385-392.
[Mine06]Mine A. The octagon abstract domain. In Proceedings of Higher-Order and Symbolic Computation.2006:31-100.
[Mine07]Mine A. The Apron Library. CEA Seminar.2007.
[Monate08]Monate B, Signoles J. Slicing for Security of Code. In Proceedings of TRUST. 2008:133-142.
[Monniaux08] Monniaux D. A Quantifier Elimination Algorithm for Linear Real Arithmetic. In Proceedings of LPAR.2008:243-257.
[Moura08]Moura LMD, Bjorner N. Z3:An Efficient SMT Solver. In Proceedings of TACAS.2008:337-340.
[Moy09]Moy Y. Automatic Modular Static Safety Checking for C Programs. Universite Paris-Sud. PhD thesis.2009:249.
[Moyl 0]Moy Y, Marche C. Modular inference of subprogram contracts for safety checking. In Proceedings of J. Symb. Comput.2010:1184-1211.
[Necula02]Necula GC, McPeak S, Rahul SP, Weimer W. CIL:Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proceedings of CC. 2002:213-228.
[Necula09]Necula G, McPeak S, Weimer W, Liblit B, Harren M. CIL:Infrastructure for C Program Analysis and Transformation.from http://www.cs.berkeley.edu/-necula/cil/CIL.pdf.2009.
[Podelski04] Podelski A, Rybalchenko A. A Complete Method for the Synthesis of Linear Ranking Functions. In Proceedings of VMCAI.2004:239-251.
[Queille82] Queille J, Sifakis J. Specification and verification of concurrent systems in CESAR. In Proceedings of Symposium on Programming.1982:337-351.
[Riazanov02] Riazanov A, Voronkov A. The design and implementation of VAMPIRE. In Proceedings of Al Commun..2002:91-110.
[Sankaranarayanan04] Sankaranarayanan S, Sipma H, Manna Z. Non-linear loop invariant generation using Grobner bases. In Proceedings of POPL.2004:318-329.
[Schmitt07] Schmitt PH, Weiβ B. Inferring Invariants by Symbolic Execution. In Proceedings of VERIFY.2007:195-210.
[Schwarz05] Schwarz B, Chen H, Wagner D, Lin J, Tu W, Morrison G, West J. Model Checking An Entire Linux Distribution for Security Violations. In Proceedings of ACSAC.2005:13-22.
[Sharmal1]Sharma R, Dillig I, Dillig T, Aiken A. Simplifying Loop Invariant Generation Using Splitter Predicates. In Proceedings of CAV.2011:703-719.
[Simon03]Simon A, King A, Howe JM. Two Variables per Linear Inequality as an Abstract Domain. In Proceedings of LOPSTR.2002:71-89.
[Wang07]Wang C, Yang Z, Gupta A, Ivancic F. Using Counterexamples for Improving the Precision of Reachability Computation with Polyhedra. In Proceedings of CAV. 2007:352-365.
[Wei11]Wei Y, Furia CA, Kazmin N, Meyer B. Inferring better contracts. In Proceedings of ICSE.2011:191-200.
[Weiser81]Weiser M. Program slicing. In Proceedings of ICSE.1981:439-449.
[Zitser04]Zitser M, Lippmann R, Leek T. Testing static analysis tools using exploitable buffer overflows from open source code. In Proceedings of SIGSOFT FSE.2004: 97-106.
[屈婉霞08]屈婉霞,李暾,郭阳,杨晓东.谓词抽象技术研究.软件学报.2008,19(1)：27-38.
[王燕妮10]王燕妮.基于不变式的软件故障检测与恢复技术研究.国防科学技术大学,硕士学位论文.2010：71.
[邢建英10]邢建英,李梦君,李舟军.CILinear:一个线性不变式自动构造工具.计算机科学.2010,37(12)：91-95.
© 2004-2018 中国地质图书馆版权所有 京ICP备05064691号 京公网安备11010802017129号 地址：北京市海淀区学院路29号 邮编：100083 电话：办公室：(+86 10)66554848；文献借阅、咨询服务、科技查新：66554700 |