多重循环程序内存访问越界增量检测方法
|
摘要
在严重威胁软件系统可靠性和安全性的多类软件缺陷中,内存访问越界属于危害性很强且广泛存在的一类缺陷,可被黑客利用并转变成多种拒绝服务漏洞和著名的缓冲区溢出等高危险性的安全漏洞。
现有的内存访问越界缺陷检测方法,对现实程序中内含复杂条件分支的多重循环,无法有效分析其内部频繁的指针运算和内存操作,因此检测效果不佳。特别是,循环执行次数无法预知而由外部输入动态确定、内存操作受循环内条件分支影响而动态变化等常见情况,对当前热门的符号执行类精确检测方法构成巨大挑战,导致该类方法在遍历程序路径实施检测时,会遇到严重的路径组合爆炸问题,即使消耗非常多时间,也常常无法正常终止。另外,现有方法被设计成对完整的程序代码实施全面检测,但现实软件系统常常会由于各种原因被更新和升级,若每次软件更新后都进行全面检测,代价过高。而且,现有方法也没有针对软件更新时容易引入新缺陷的代码区域进行专门检测,因此大部分检测时间被花费在无意义的重复检测之中。经分析,其问题根源是:现有符号执行类方法单纯追求代码覆盖率而缺陷针对性不强。
因此,提出了一种面向多重循环程序的内存访问越界缺陷增量检测方法。针对内存访问越界缺陷与循环归纳变量运算紧密关联的特点,首次将递推链扩展代数与符号执行类缺陷检测方法相结合,设计了面向多重循环的缺陷检测指导信息,同时利用软件更新影响的局部性特点,实现了基于路径指导的定向检测和基于更新影响的增量检测。其主要算法如下:
1)根据软件更新对源代码的文本修改,结合控制与数据依赖分析,识别受软件更新实际影响的语义变化区域。有针对性地在该区域中分析多重循环中指针运算和内存读写模式,初步识别出内存访问越界疑似缺陷,再根据控制与数据依赖关系标记出疑似缺陷所依赖的语句和变量,作为缺陷依赖区域,构造能充分检测软件更新引入缺陷的相关执行要素最小集合——精简检测流图,及早排除与缺陷检测无关的语句。
2)基于精简检测流图进行多重循环分析,跟踪和分析多重循环中缺陷依赖变量的递推关系,将其统一表示为递推链扩展代数的形式,再根据该代数规则进行符号操作,从而推导出缺陷依赖变量的值或上下界的闭形式函数,构建循环摘要和函数摘要。接着,根据内存范围等安全性限制条件,利用循环摘要和函数摘要,构造缺陷触发条件并求解,从而判断缺陷触发的可能性,及时排除疑似缺陷集合中的误报,还可推断出用于预测和选取缺陷关联路径的缺陷检测指导信息。
3)根据路径选取方向性、条件分支检测优先级、各个循环的有效迭代次数范围等缺陷检测指导信息,有指导地以按需符号执行方式实施路径敏感和位运算级精度的缺陷定向检测。每次经过疑似缺陷点时,主动检测缺陷触发条件,并结合在检测路径上收集的路径分支条件进行约束求解,通过判断触发路径的条件可满足性来进一步避免缺陷误报。而每次在路径分叉点,按需克隆执行环境以避免相同路径前缀的重复执行,并立即求解所选取分支的路径条件集,以及时剪除不可行的路径分支。最后,生成无误报的缺陷集合、能真实触发这些缺陷的程序输入集合以及相应的触发路径集合,作为缺陷并非误报的验证信息。
基于上述算法,设计和实现了能面向多重循环程序实施内存访问越界缺陷增量检测的原型系统,并在国内首次将微软主流编译器的下一代工业级编译平台Phoenix用于软件缺陷检测,作为该系统的基础支撑环境。该系统已检测Filezilla Server、SpamAssassin、WGet和OpenSSL等多个知名开源软件,找到了真实的代码缺陷。
实验结果表明,利用递推链扩展代数进行多重循环分析,有指导地以符号执行方式实施定向检测,能够克服多重循环程序对现有符号执行类方法造成的困难,包括循环次数由输入确定、内存操作受循环内条件分支影响等难题,既避免了盲目路径遍历,又保持了路径敏感和位运算级的检测精度,提高了检测效率和准确性。同时,利用软件更新影响的局部性特点,实现缺陷增量检测,提高了检测时效性和针对性。另外,该方法能够在检测和定位内存访问越界缺陷同时,生成相应的程序输入和触发路径等验证信息,这在软件安全性测试和信息对抗等领域有很大的应用价值。
Memory overrun belongs to a kind of dangerous and universal defects among several kinds of defect which are able to compromise safety and security of software system seriously.By it,Hackers can cause many types of denial-of-service vulnerabilities and very dangerous security vulnerabilities including infamous buffer overflow.
Current detection methods for memory overrun are unable to efficiently analyze frequent pointer arithmetic and memory operations in multi-loops with complicated conditional branches of real programs,thus their detection effects are not good enough.Such usual cases as unpredictable loop iteration numbers determined dynamically by input and memory operations controlled dynamically by conditional branches in multi-loops etc.,pose great challenges against popular precise detection methods based on symbolic execution.Therefor,these methods will encounter serious problem of path combination explosion when traversing program paths for full detection,so that they are unable to terminate normally even if very much time is spent.In addition,the current methods are designed to detect full source code,but real software systems are often updated for many reasons,it is over-expensive if source code is fully detected after each software update.Moreover,the current methods don't detect specially the code region where new defects caused by updates occur probably;therefore most time is spent in meaningless repeat detections.The root cause of these problems is analyzed and concluded to be that the current symbolic execution methods try best to achieve high code coverage without enough pertinence as to defects.
Thereby,the incremental detection method for memory overrun in multi-loop programs is presented.According to the characteristic of tight correlation between memory overrun and loop induction variable arithmetic,extended algebra for chains of recurrences is combined with detection methods based on symbolic execution,for the first time,to design defect detection guide information as to multi-loop,while locality characteristic of software updates and their impact is used.Thus,directed detection based on path guide and incremental detection based on update impact is implemented,whose main algorithms are as follows:
1) According to textual modification in source code caused by software update, after control/data-dependence analysis,semantic difference regions are identified.By analyzing pointer arithmetic and memory operations in multi-loop pertinently,suspect defects of memory overrun are primarily identify.Based on control/data-dependence relation,instructions and variables dependent by suspect defects are marked as defect dependent regions,thus FACE(Flow grAph for Condensed Examining) is built,which is minimum set of correlative execution elements capable of detecting defects caused by updates adequately,to preclude instructions irrespective of defect detection as soon as possible.
2) Based on FACE,multi-loops are analyzed by a) tracing recurrent relations of defect dependent variables in multi-loop,b) expressing them uniformly as CR#(extended algebra for chains of recurrences) form,c) operating them symbolically based on CR# algebra rule,d) deduce closed-form functions of value or range limit of defect dependent variables,e) construct loop summary and function summary.Next,by combining safety restriction condition e.g.memory range with loop summary and function summary, defect trigger conditions are built and solved to estimate probabilities of defect triggering for precluding false positive in suspect defect set,and infer defect detection guide information for predicting defect relative paths.
3) According to guide information such as path direction,branch priority, available range of loop iteration etc.,path-sensitive and bit-precise directed detection is applied,based on on-demand symbolic execution.At each suspect defect point,the defect trigger condition is actively detected and solved together with path conditions to determine condition satisfiabilities and preclude more false positive.At each path branch point,the executive context is on-demand cloned to avoid re-executing the same path prefix of several paths,and path conditions of selected branch are solved in time to prune infeasible paths.Lastly,defect set and corresponding set of defect-triggering input and execution paths are automatically generated as verification information.
Accordingly,the incremental detection prototype system for memory overrun in multi-loop programs is designed and implemented.For the first time in China, Phoenix,next-generation industry-level compiler infrastructure of Microsoft mainstream compiler,is used for software defect detection,as basic underlay platform of the system.The system has been tested on several open source software such as Filezilla Server,SpamAssassin,WGet and OpenSSL,and found real defects.
The experiment results show that by CR# analysis in multi-loop and defect directed detection,the algorithm can overcome the multi-loop problems encountered by current symbolic execution methods,including number of loop iteration determined by input,memory operations controlled by conditional branches in loop etc..Thus,it avoids blind path traversal while achieving path-sensitive and bit-precise detection,and improves efficiency and accuracy of detection.Moreover, incremental detection based on locality characteristic of software updates and their impact is applied to improve detection pertinence.In addition,it is of important application value in the field of software security testing and information counterwork that the algorithm can automatically generate sets of true defect, defect-triggering input and execution paths
现有的内存访问越界缺陷检测方法,对现实程序中内含复杂条件分支的多重循环,无法有效分析其内部频繁的指针运算和内存操作,因此检测效果不佳。特别是,循环执行次数无法预知而由外部输入动态确定、内存操作受循环内条件分支影响而动态变化等常见情况,对当前热门的符号执行类精确检测方法构成巨大挑战,导致该类方法在遍历程序路径实施检测时,会遇到严重的路径组合爆炸问题,即使消耗非常多时间,也常常无法正常终止。另外,现有方法被设计成对完整的程序代码实施全面检测,但现实软件系统常常会由于各种原因被更新和升级,若每次软件更新后都进行全面检测,代价过高。而且,现有方法也没有针对软件更新时容易引入新缺陷的代码区域进行专门检测,因此大部分检测时间被花费在无意义的重复检测之中。经分析,其问题根源是:现有符号执行类方法单纯追求代码覆盖率而缺陷针对性不强。
因此,提出了一种面向多重循环程序的内存访问越界缺陷增量检测方法。针对内存访问越界缺陷与循环归纳变量运算紧密关联的特点,首次将递推链扩展代数与符号执行类缺陷检测方法相结合,设计了面向多重循环的缺陷检测指导信息,同时利用软件更新影响的局部性特点,实现了基于路径指导的定向检测和基于更新影响的增量检测。其主要算法如下:
1)根据软件更新对源代码的文本修改,结合控制与数据依赖分析,识别受软件更新实际影响的语义变化区域。有针对性地在该区域中分析多重循环中指针运算和内存读写模式,初步识别出内存访问越界疑似缺陷,再根据控制与数据依赖关系标记出疑似缺陷所依赖的语句和变量,作为缺陷依赖区域,构造能充分检测软件更新引入缺陷的相关执行要素最小集合——精简检测流图,及早排除与缺陷检测无关的语句。
2)基于精简检测流图进行多重循环分析,跟踪和分析多重循环中缺陷依赖变量的递推关系,将其统一表示为递推链扩展代数的形式,再根据该代数规则进行符号操作,从而推导出缺陷依赖变量的值或上下界的闭形式函数,构建循环摘要和函数摘要。接着,根据内存范围等安全性限制条件,利用循环摘要和函数摘要,构造缺陷触发条件并求解,从而判断缺陷触发的可能性,及时排除疑似缺陷集合中的误报,还可推断出用于预测和选取缺陷关联路径的缺陷检测指导信息。
3)根据路径选取方向性、条件分支检测优先级、各个循环的有效迭代次数范围等缺陷检测指导信息,有指导地以按需符号执行方式实施路径敏感和位运算级精度的缺陷定向检测。每次经过疑似缺陷点时,主动检测缺陷触发条件,并结合在检测路径上收集的路径分支条件进行约束求解,通过判断触发路径的条件可满足性来进一步避免缺陷误报。而每次在路径分叉点,按需克隆执行环境以避免相同路径前缀的重复执行,并立即求解所选取分支的路径条件集,以及时剪除不可行的路径分支。最后,生成无误报的缺陷集合、能真实触发这些缺陷的程序输入集合以及相应的触发路径集合,作为缺陷并非误报的验证信息。
基于上述算法,设计和实现了能面向多重循环程序实施内存访问越界缺陷增量检测的原型系统,并在国内首次将微软主流编译器的下一代工业级编译平台Phoenix用于软件缺陷检测,作为该系统的基础支撑环境。该系统已检测Filezilla Server、SpamAssassin、WGet和OpenSSL等多个知名开源软件,找到了真实的代码缺陷。
实验结果表明,利用递推链扩展代数进行多重循环分析,有指导地以符号执行方式实施定向检测,能够克服多重循环程序对现有符号执行类方法造成的困难,包括循环次数由输入确定、内存操作受循环内条件分支影响等难题,既避免了盲目路径遍历,又保持了路径敏感和位运算级的检测精度,提高了检测效率和准确性。同时,利用软件更新影响的局部性特点,实现缺陷增量检测,提高了检测时效性和针对性。另外,该方法能够在检测和定位内存访问越界缺陷同时,生成相应的程序输入和触发路径等验证信息,这在软件安全性测试和信息对抗等领域有很大的应用价值。
Memory overrun belongs to a kind of dangerous and universal defects among several kinds of defect which are able to compromise safety and security of software system seriously.By it,Hackers can cause many types of denial-of-service vulnerabilities and very dangerous security vulnerabilities including infamous buffer overflow.
Current detection methods for memory overrun are unable to efficiently analyze frequent pointer arithmetic and memory operations in multi-loops with complicated conditional branches of real programs,thus their detection effects are not good enough.Such usual cases as unpredictable loop iteration numbers determined dynamically by input and memory operations controlled dynamically by conditional branches in multi-loops etc.,pose great challenges against popular precise detection methods based on symbolic execution.Therefor,these methods will encounter serious problem of path combination explosion when traversing program paths for full detection,so that they are unable to terminate normally even if very much time is spent.In addition,the current methods are designed to detect full source code,but real software systems are often updated for many reasons,it is over-expensive if source code is fully detected after each software update.Moreover,the current methods don't detect specially the code region where new defects caused by updates occur probably;therefore most time is spent in meaningless repeat detections.The root cause of these problems is analyzed and concluded to be that the current symbolic execution methods try best to achieve high code coverage without enough pertinence as to defects.
Thereby,the incremental detection method for memory overrun in multi-loop programs is presented.According to the characteristic of tight correlation between memory overrun and loop induction variable arithmetic,extended algebra for chains of recurrences is combined with detection methods based on symbolic execution,for the first time,to design defect detection guide information as to multi-loop,while locality characteristic of software updates and their impact is used.Thus,directed detection based on path guide and incremental detection based on update impact is implemented,whose main algorithms are as follows:
1) According to textual modification in source code caused by software update, after control/data-dependence analysis,semantic difference regions are identified.By analyzing pointer arithmetic and memory operations in multi-loop pertinently,suspect defects of memory overrun are primarily identify.Based on control/data-dependence relation,instructions and variables dependent by suspect defects are marked as defect dependent regions,thus FACE(Flow grAph for Condensed Examining) is built,which is minimum set of correlative execution elements capable of detecting defects caused by updates adequately,to preclude instructions irrespective of defect detection as soon as possible.
2) Based on FACE,multi-loops are analyzed by a) tracing recurrent relations of defect dependent variables in multi-loop,b) expressing them uniformly as CR#(extended algebra for chains of recurrences) form,c) operating them symbolically based on CR# algebra rule,d) deduce closed-form functions of value or range limit of defect dependent variables,e) construct loop summary and function summary.Next,by combining safety restriction condition e.g.memory range with loop summary and function summary, defect trigger conditions are built and solved to estimate probabilities of defect triggering for precluding false positive in suspect defect set,and infer defect detection guide information for predicting defect relative paths.
3) According to guide information such as path direction,branch priority, available range of loop iteration etc.,path-sensitive and bit-precise directed detection is applied,based on on-demand symbolic execution.At each suspect defect point,the defect trigger condition is actively detected and solved together with path conditions to determine condition satisfiabilities and preclude more false positive.At each path branch point,the executive context is on-demand cloned to avoid re-executing the same path prefix of several paths,and path conditions of selected branch are solved in time to prune infeasible paths.Lastly,defect set and corresponding set of defect-triggering input and execution paths are automatically generated as verification information.
Accordingly,the incremental detection prototype system for memory overrun in multi-loop programs is designed and implemented.For the first time in China, Phoenix,next-generation industry-level compiler infrastructure of Microsoft mainstream compiler,is used for software defect detection,as basic underlay platform of the system.The system has been tested on several open source software such as Filezilla Server,SpamAssassin,WGet and OpenSSL,and found real defects.
The experiment results show that by CR# analysis in multi-loop and defect directed detection,the algorithm can overcome the multi-loop problems encountered by current symbolic execution methods,including number of loop iteration determined by input,memory operations controlled by conditional branches in loop etc..Thus,it avoids blind path traversal while achieving path-sensitive and bit-precise detection,and improves efficiency and accuracy of detection.Moreover, incremental detection based on locality characteristic of software updates and their impact is applied to improve detection pertinence.In addition,it is of important application value in the field of software security testing and information counterwork that the algorithm can automatically generate sets of true defect, defect-triggering input and execution paths
引文
[1]J.C.Foster,V.Osipov,and N.Bhalla,Buffer Overflow Attacks:Syngress,2005.
[2]M.W.Eichin and J.A.Rochlis,“With microscope and tweezers:an analysis of the Internet virus of Nov.1988,”Proceedings of the IEEE Symp.Security and Privacy,1989.
[3]“Common Vulnerabilities and Exposures.”,http://cve.mitre.org.
[4]“Ph4nt0m Security Team.”,http://www.ph4nt0m.org
[5]R.Hastings and B.Joyce,“Purify:Fast detection of memory leaks and access errors.,”in Proceedings of the Winter USENIX Conference,1992.
[6]C.N.George,C.Jeremy,H.Matthew,M.Scott,and W.Westley,“CCured:type-safe retrofitting of legacy software,”ACM Trans.Program.Lang.Syst,vol.27,pp.477-526,2005.
[7]H.Etoh,“GCC Extension for Protecting Applications from Stack-smashing Attacks.,”2005,http://www.trl.ibm.com/projects/security/ssp/.
[8]W.Robertson,C.Kruegel,D.Mute,and F.Valeur,“Run-time Detection of Heap-based Overflows,”in Proceedings of the 17th USENIX conference on System administration San Diego,CA:USENIX Association,2003.
[9]D.Larochelle and D.Evans,“Statically detecting likely buffer overflow vulnerabilities,”in Proceedings of the 10th conference on USENIX Security Symposium-Volume 10 Washington,D.C.:USENIX Association,2001.
[10]N.Dor,M.Rodeh,and M.Sagiv,“CSSV:Towards a realistic tool for statically detecting all buffer overflows in C,”Acm Sigplan Notices,vol.38,pp.155-167,May 2003.
[11]D.Wagner,J.S.Foster,E.A.Brewer,and A.Aiken,“A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities,”in Proceedings of the 2000 Network and Distributed Systems Security Conference San Diego,CA,2000.
[12]C.Flanagan,K.R.M.Leino,M.Lillibridge,G Nelson,J.B.Saxe,and R.Stata,“Extended static checking for Java,”in Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation Berlin,Germany:ACM,2002.
[13]K.Ashcraft and D.Engler,“Using Programmer-Written Compiler Extensions to Catch Security Holes,”in Proceedings of the 2002 IEEE Symposium on Security and Privacy:IEEE Computer Society,2002.
[14]X.Yichen and A.Alex,“Saturn:A scalable framework for error detection using Boolean satisfiability,”ACM Trans.Program.Lang.Syst,vol.29,p.16,2007.
[15]W.R.Bush,J.D.Pincus,and D.J.Sielaff,“A static analyzer for finding dynamic programming errors,”Softw.Pract.Exper.,vol.30,pp.775-802,2000.
[16]Y.Xie,A.Chou,and D.Engler,“ARCHER:using symbolic,path-sensitive analysis to detect memory access errors,”in Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering Helsinki,Finland:ACM,2003.
[17]P.Godefroid,N.Klarlund,and K.Sen,“DART:Directed automated random testing,”Acm Sigplan Notices,vol.40,pp.213-223,Jun 2005.
[18]K.Sen and G.Agha,“CUTE and jCUTE:Concolic unit testing and explicit path model-checking tools,”Computer Aided Verification,Proceedings,vol.4144,pp.419-423,2006.
[19]C.Cadar,V.Ganesh,P.M.Pawlowski,D.L.Dill,and D.R.Engler,“EXE:Automatically Generating Inputs of Death,”ACM Trans.Inf.Syst.Secur.,vol.12,pp.1-38,2008.
[20]C.Cristian,G Vijay,M.P.Peter,L.D.David,and R.E.Dawson,“EXE:automatically generating inputs of death,”in Proceedings of the 13th ACM conference on Computer and communications security Alexandria,Virginia,USA:ACM,2006.
[21]J.Yang,C.Sar,P.Twohey,C.Cadar,and D.Engler,“Automatically Generating Malicious Disks using Symbolic Execution,”in Proceedings of the 2006 IEEE Symposium on Security and Privacy:IEEE Computer Society,2006.
[22]P.Godefroid,“Compositional dynamic test generation,”in Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages Nice,France:ACM,2007.
[23]P.Godefroid,M.Y.Levin,and D.Molnar,“Automated Whitebox Fuzz Testing,”in Proceedings of NDSS'2008(Network and Distributed Systems Security)San Diego,2008,pp.151-166.
[24]C.Cadar,D.Dunbar,and D.Engler,“Klee:Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs,”in Operating System Design and Implementation(OSDI),2008.
[25]S.Anand,P.Godefroid,and N.Tillmann,“Demand-Driven Compositional Symbolic Execution,”in Tools and Algorithms for the Construction and Analysis of Systems,2008,pp.367-381.
[26]P.Godefroid,A.Kiezun,and M.Y.Levin,“Grammar-based whitebox fuzzing,”in Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation Tucson,AZ,USA:ACM,2008.
[27]A.V.Aho,R.Semi,and J.D.Ullman,Compilers:principles,techniques,and tools:Addison-Wesley Longman Publishing Co.,Inc.,1986.
[28]T.Fahringer,“Efficient Symbolic Analysis for Parallelizing Compilers and Performance Estimators,”J.Supercomput.,vol.12,pp.227-252,1998.
[29]M.R.Haghighat and C.D.Polychronopoulos,“Symbolic analysis for parallelizing compilers,”ACM Trans.Program.Lang.Syst,vol.18,pp.477-518,1996.
[30]M.P.Gerlek,E.Stoltz,and M.Wolfe,“Beyond induction variables:detecting and classifying sequences using a demand-driven SSA form,”ACM Trans.Program.Lang.Syst.,vol.17,pp.85-122,1995.
[31]M.R.Haghighat and C.D.Polychronopoulos,“Symbolic Program Analysis and Optimization for Parallelizing Compilers,”in Proceedings of the 5th International Workshop on Languages and Compilers for Parallel Computing:Springer-Verlag,1993.
[32]Z.Li,P.-C.Yew,and C.-Q.Zhu,“Data dependence analysis on multi-dimensional array references,”in Proceedings of the 3rd international conference on Supercomputing Crete,Greece:ACM,1989.
[33]R.Allen and K.Kennedy,Optimizing Compilers for Modern Architectures.San Fransisco,CA:Morgan Kaufmann,2002.
[34]S.Muchnick,Advanced Compiler Design and Implementation.San Fransisco,CA:Morgan Kaufmann,1997.
[35]U.BANERJEE,Dependence Analysis for Supercomputing.Boston:Kluwer,1988.
[36]M.BURKE and R.CYTRON,“Interprocedural dependence analysis and parallelization,”in proceedings of the Symposium on Compiler Construction 1986,pp.162-175.
[37]G.GOFF,K.KENNEDY,and C.-W.TSENG,“Practical dependence testing,”in proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI),Toronto,Ontario,Canada,1991,pp.15-29.
[38]D.KUCK,The Structure of Computers and Computations vol.1.New York:John Wiley and Sons,1987.
[39]D.E.MAYDAN,J.L.HENNESSY,and M.S.LAM,“Efficient and exact data dependence analysis,”in proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI),1991,pp.1-14.
[40]K.PSARRIS and K.KYRIAKOPOULOS,“Measuring the accuracy and efficiency of the data dependence tests,”in proceedings of the International Conference on Parallel and Distributed Computing Systems,2001.
[41]R.RUGINA and M.RINARD,“Symbolic bounds analysis of array indices,and accessed memory regions,”in proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI),Vancouver,British Columbia,Canada,2000,pp.182-195.
[42]Z.SHEN,Z.LI,and P.C.YEW,“An empirical study on array subscripts and data dependencies,”in proceedings of the International Conference on Parallel Processing,1989,pp.145-152.
[43]M.WOLFE,High Performance Compilers for Parallel Computers.Redwood City,CA:Addison-Wesley,1996.
[44]H.ZIMA and B.CHAPMAN,Supercompilers for Parallel and Vector Computers.New York:ACM Press,1990.
[45]Z.Ammarguellat and I.W.L.Harrison,“Automatic recognition of induction variables and recurrence relations by abstract interpretation,”in Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation White Plains,New York,United States:ACM,1990.
[46]K.PSARRIS,“Program analysis techniques for transforming programs for parallel systems” Parallel Computing vol.28,pp.455-469,2003.
[47]K.Psarris and K.Kyriakopoulos,“The impact of data dependence analysis on compilation and program parallelization,”in Proceedings of the 17th annual international conference on Supercomputing San Francisco,CA,USA:ACM,2003.
[48]P.Wu,A.Cohen,J.Hoeflinger,and D.Padua,“Monotonic evolution:an alternative to induction variable substitution for dependence analysis,”in Proceedings of the 15th international conference on Supercomputing Sorrento,Italy:ACM,2001.
[49]R.A.v.Engelen,J.Birch,Y.Shou,B.Walsh,and K.A.Gallivan,“A unified framework for nonlinear dependence testing and symbolic analysis,”in Proceedings of the 18th annual international conference on Supercomputing Malo,France:ACM,2004.
[50]Y.Shou,R.A.v.Engelen,J.Birch,and K.A.Gallivan,“Toward efficient flow-sensitive induction variable analysis and dependence testing for loop optimization,”in Proceedings of the 44th annual Southeast regional conference Melbourne,Florida:ACM,2006.
[51]R.v.Engelen,“The CR# Algebra and its Application in Loop Analysis and Optimization,” Technical Report2004.
[52]E.V.Zima,“Recurrent Relations and Speed-up of Computations Using Computer Algebra Systems,”in Proceedings of the International Symposium on Design and Implementation of Symbolic Computation Systems:Springer-Verlag,1993.
[53]E.V.Zima,“On computational properties of chains of recurrences,”in Proceedings of the 2001 international symposium on Symbolic and algebraic computation London,Ontario,Canada:ACM,2001.
[54]O.Bachmann,“Chains of recurrences,”Kent State University,1997.
[55]O.Bachmann,P.S.Wang,and E.V.Zima,“Chains of recurrences:a method to expedite the evaluation of closed-form functions,”in Proceedings of the international symposium on Symbolic and algebraic computation Oxford,United Kingdom:ACM,1994.
[56]O.Bachmann,“MPCR:an efficient and flexible chains of recurrences server,”SIGSAM Bull.,vol.31,pp.15-21,1997.
[57]R.A.v.Engelen,J.Birch,and K.A.Gallivan,“Array Data Dependence Testing with the Chains of Recurrences Algebra,”in Proceedings of the Innovative Architecture for Future Generation High-Performance Processors and Systems:IEEE Computer Society,2004.
[58]J.L.Birch,“Methods for linear and nonlinear array data dependence analysis with the chains of recurrences algebra,”Florida State University,2007,p.233.
[59]V.Kislenkov,V.Mitrofanov,and E.Zima,“Multidimensional chains of recurrences,”in Proceedings of the 1998 international symposium on Symbolic and algebraic computation Rostock,Germany:ACM,1998.
[60]B.Beizer,Software Testing Techniques,2nd ed.New York:van Nostrand Reinhold,1990.
[61]H.Agrawal,J.R.Horgan,E.W.Krauser,and S.A.London,“Incremental regression testing,”in Software Maintenance,1993.CSM-93,Proceedings.,Conference on,1993,pp.348-357.
[62]Y.-F.Chen,D.S.Rosenblum,and K.-P.Vo,“TestTube:a system for selective regression testing,”in Proceedings of the 16th international conference on Software engineering Sorrento,Italy:IEEE Computer Society Press,1994.
[63]E.Engstr\,\#246,M.Skoglund,and P.Runeson,“Empirical evaluations of regression test selection techniques:a systematic review,”in Proceedings of the Second ACM-IEEE international symposium on Empirical software engineering and measurement Kaiserslautern,Germany:ACM,2008.
[64]P.K.Chittimalli and M.J.Harrold,“Regression test selection on system requirements,”in Proceedings of the 1st conference on India software engineering conference Hyderabad,India:ACM,2008.
[65]G.Rothermel,S.Elbaum,A.G.Malishevsky,P.Kallakuri,and X.Qiu,“On test suite composition and cost-effective regression testing,”ACM Trans.Softw.Eng.Methodol.,vol.13,pp.277-331,2004.
[66]M.J.Harrold,J.A.Jones,T.Li,D.Liang,A.Orso,M.Pennings,S.Sinha,S.A.Spoon,and A.Gujarathi,“Regression test selection for Java software,”in Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming,systems,languages,and applications Tampa Bay,FL,USA:ACM,2001.
[67]T.L.Graves,M.J.Harrold,J.-M.Kim,A.Porter,and G.Rothermel,“An empirical study of regression test selection techniques,”ACM Trans.Softw.Eng.Methodol.,vol.10,pp.184-208,2001.
[68]J.Bible,G.Rothermel,and D.S.Rosenblum,“A comparative study of coarse-and fine-grained safe regression test-selection techniques,”ACM Trans.Softw.Eng.Methodol.,vol.10,pp.149-183,2001.
[69]F.I.Vokolos and P.G Frankl,“Empirical evaluation of the textual differencing regression testing technique,”in Software Maintenance,1998.Proceedings.International Conference on,1998,pp.44-53.
[70]R.Gregg and H.Mary Jean,“A safe,efficient regression test selection technique,”ACM Trans.Softw.Eng.Methodol.,vol.6,pp.173-210,1997.
[71]D.Jeffrey and N.Gupta,“Experiments with test case prioritization using relevant slices,”J.Syst.Softw.,vol.81,pp.196-221,2008.
[72]K.K.Aggrawal,Y.Singh,and A.Kaur,“Code coverage based technique for prioritizing test cases for regression testing,”SIGSOFT Softw.Eng.Notes,vol.29,pp.1-4,2004.
[73]A.Srivastava and J.Thiagarajan,“Effectively prioritizing tests in development environment,”in Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis Roma,Italy:ACM,2002.
[74]S.Elbaum,A.G Malishevsky,and G Rothermel,“Prioritizing test cases for regression testing,”in Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis Portland,Oregon,United States:ACM,2000.
[75]H.Zhong,L.Zhang,and H.Mei,“An experimental study of four typical test suite reduction techniques,”Inf.Softw.Technol.,vol.50,pp.534-546,2008.
[76]Y.Chen,R.L.Probert,and H.Ural,“Regression test suite reduction using extended dependence analysis,”in Fourth international workshop on Software quality assurance:in conjunction with the 6th ESEC/FSE joint meeting Dubrovnik,Croatia:ACM,2007.
[77]W.E.Wong,J.R.Horgan,S.London,and A.P.Mathur,“Effect of test set minimization on fault detection effectiveness,”Softw.Pract.Exper.,vol.28,pp.347-369,1998.
[78]R.Gregg,H.M.Jean,O.Jeffery,and H.Christine,“An Empirical Study of the Effects of Minimization on the Fault Detection capabilities of Test Suites,”Oregon State University1998.
[79]M.J.Harrold,R.Gupta,and M.L.Soffa,“A methodology for controlling the size of a test suite,”ACM Trans.Softw.Eng.Methodol.,vol.2,pp.270-285,1993.
[80]J.W.Hunt and M.D.Mcllroy,“An Algorithm for Differential File Comparison,”Bell Laboratories 1976.
[81]J.I.Maletic and M.L.Collard,“Supporting Source Code Difference Analysis,”in Proceedings of the 20th IEEE International Conference on Software Maintenance:IEEE Computer Society,2004.
[82]R.Cytron,J.Ferrante,B.K.Rosen,M.N.Wegman,and F.K.Zadeck,“An efficient method of computing static single assignment form,”in Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages Austin,Texas,United States:ACM,1989.
[83]R.Kennedy,S.Chan,S.-M.Liu,R.Lo,P.Tu,and F.Chow,“Partial redundancy elimination in SSA form,”ACM Trans.Program.Lang.Syst,vol.21,pp.627-676,1999.
[84]M.M.Brandis and H.Mossenbock,“Single-pass generation of static single-assignment form for structured languages,”ACM Trans.Program.Lang.Syst,vol.16,pp.1684-1698,1994.
[85]H.Srinivasan,J.Hook,and M.Wolfe,“Static single assignment for explicitly parallel programs,”in Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages Charleston,South Carolina,United States:ACM,1993.
[86]C.McConnell and R.E.Johnson,“Using static single assignment form in a code optimizer,” ACM Lett.Program.Lang.Syst.,vol.1,pp.152-160,1992.
[87]R.Cytron,J.Ferrante,B.K.Rosen,M.N.Wegman,and F.K.Zadeck,“Efficiently computing static single assignment form and the control dependence graph,”ACM Trans.Program.Lang.Syst.,vol.13,pp.451-490,1991.
[88]P.Briggs,K.D.Cooper,and L.Torczon,“Rematerialization,”in Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation San Francisco,California,United States:ACM,1992.
[89]M.N.Wegman and F.K.Zadeck,“Constant propagation with conditional branches,”ACM Trans.Program.Lang.Syst,vol.13,pp.181-210,1991.
[90]F.Jeanne,J.O.Karl,and D.W.Joe,“The program dependence graph and its use in optimization,”ACM Trans.Program.Lang.Syst.,vol.9,pp.319-349,1987.
[91]T.Y.Chen and Y.Y.Cheung,“Structural Properties of Post-Dominator Trees,”in Proceedings of the Australian Software Engineering Conference:IEEE Computer Society,1997.
[92]V.C.Sreedhar,G R.Gao,and Y.-f.Lee,“Incremental computation of dominator trees,”in Papers from the 1995 ACM SIGPLAN workshop on Intermediate representations San Francisco,California,United States:ACM,1995.
[93]G.Ramalingam and T.Reps,“An incremental algorithm for maintaining the dominator tree of a reducible flowgraph,”in Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages Portland,Oregon,United States:ACM,1994.
[94]B.D.Sutter,L.V.Put,and K.D.Bosschere,“A practical interprocedural dominance algorithm,”ACM Trans.Program.Lang.Syst,vol.29,p.19,2007.
[95]S.Horwitz and T.Reps,“The Use Of Program Dependence Graphs In Software Engineering,”in Software Engineering,1992.International Conference on,1992,pp.392-411.
[96]K.B.Gallagher,“Some notes on interprocedural program slicing,”in Source Code Analysis and Manipulation,2004.Fourth IEEE International Workshop on,2004,pp.36-42.
[97]R.Gopal,“Dynamic program slicing based on dependence relations,”in Software Maintenance,1991.,Proceedings.Conference on,1991,pp.191-200.
[98]R.Johnson and K.Pingali,“Dependence-based program analysis,”in Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation Albuquerque,New Mexico,United States:ACM,1993.
[99]G.Ramalingam,“On loops,dominators,and dominance frontiers,”ACM Trans.Program.Lang.Syst,vol.24,pp.455-490,2002.
[100]G.Ramalingam,“On loops,dominators,and dominance frontier,”SIGPLAN Not.,vol.35,pp.233-241,2000.
[101]L.Heng,W.K.Chan,and T.H.Tse,“Static Slicing for Pervasive Programs,”in Quality Software,2006.QSIC 2006.Sixth International Conference on,2006,pp.185-192.
[102]Z.Yingzhou,X.Baowen,and J.E.Labra Gayo,“A formal method for program slicing,”in Software Engineering Conference,2005.Proceedings.2005 Australian,2005,pp.140-148.
[103]D.Binkley,S.Danicic,T.Gyimothy,M.A.H.M.Harman,A.A.K.A.Kiss,and B.A.K.B.Korel,“Minimal slicing and the relationships between forms of slicing,”in Source Code Analysis and Manipulation,2005.Fifth IEEE International Workshop on,2005,pp.45-54.
[104]F.Umemori,K.Konda,R.Yokomori,and K.A.I.K.Inoue,“Design and implementation of bytecode-based Java slicing system,”in Source Code Analysis and Manipulation,2003.Proceedings.Third IEEE International Workshop on,2003,pp.108-117.
[105]A.R.Kulkarni and S.Ramesh,“Static slicing of reactive programs,”in Source Code Analysis and Manipulation,2003.Proceedings.Third IEEE International Workshop on,2003,pp.98-107.
[106]J.Rilling and B.Karanth,“A hybrid program slicing framework,”in Source Code Analysis and Manipulation,2001.Proceedings.First IEEE International Workshop on,2001,pp.12-23.
[107]P.Kilpatrick,D.Crookes,and M.Owens,“Program slicing:a computer aided programming technique,”in Software Engineering,1988 Software Engineering 88.,Second IEE/BCS Conference:,1988,pp.60-64.
[108]J.C.Hwang,M.W.Du,and C.R.Chou,“The influence of language semantics on program slices,”in Computer Languages,1988.Proceedings.,International Conference on,1988,pp.120-127.
[109]E.V.Zima,“Automatic construction of systems of recurrence relations,”USSR Computational Mathematics and Mathematical Physics,pp.193-197,1986.
[110]E.V.Zima,“Simplification and optimization transformations of chains of recurrences,”in proceedings of the International Symposium on Symbolic and Algebraic Computing,Montreal,Canada,1995.
[111]R.v.Engelen,“Efficient Symbolic Analysis for Optimizing Compilers,”in proceedings of the ETAPS International Conference on Compiler Construction(CC),2001,pp.118-132.
[112]R.v.Engelen,“Symbolic Evaluation of Chains of Recurrences for Loop Optimization,” Technical Report TR-000102,2000.
[113]Y.Shou,R.Engelen,and J.Birch,“Flow-Sensitive Loop-Variant Variable Classification in Linear Time,”in Languages and Compilers for Parallel Computing:20th International Workshop,LCPC 2007,Urbana,IL,USA,October 11-13,2007,Revised Selected Papers:Springer-Verlag,2008,pp.323-337.
[114]J.Birch,R.A.v.Engelen,K.A.Gallivan,and Y.Shou,“An empirical evaluation of chains of recurrences for array dependence testing,”in Proceedings of the 15th international conference on Parallel architectures and compilation techniques Seattle,Washington,USA:ACM,2006.
[115]D.Detlefs,G.Nelson,and J.B.Saxe,“Simplify:a theorem prover for program checking,”J.ACM,vol.52,pp.365-473,2005.
[116]T.Ball,B.Cook,S.K.Lahiri,and L.Zhang,“Zapato:Automatic Theorem Proving for Predicate Abstraction Refinement,”in Computer Aided Verification,2004,pp.457-461.
[117]J.P.Marques-Silva and K.A.Sakallah,“GRASP:a search algorithm for propositional satisfiability,”Computers,IEEE Transactions on,vol.48,pp.506-521,1999.
[118]H.Zhang,“SATO:An efficient prepositional prover,”in Automated Deduction—CADE-14,1997,pp.272-275.
[119]M.W.Moskewicz,C.F.Madigan,Y.Zhao,L.Zhang,and S.Malik,“Chaff:engineering an efficient SAT solver,”in Design Automation Conference,2001.Proceedings,2001,pp.530-535.
[120]S.A.Cook,“The complexity of theorem-proving procedures,”in Proceedings of the third annual ACM symposium on Theory of computing Shaker Heights,Ohio,United States:ACM,1971.
[121]K.R.Apt,“Some Remarks on Boolean Constraint Propagation,”in Selected papers from the Joint ERCIM/Compulog Net Workshop on New Trends in Contraints:Springer-Verlag,2000.
[122]L.Shuvendu and Q.Shaz,“Back to the future:revisiting precise program verification using SMT solvers,”in Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages San Francisco,California,USA:ACM,2008.
[123]L.de Moura and N.Bjwner,“Z3:An Efficient SMT Solver,”in Tools and Algorithms for the Construction and Analysis of Systems,2008,pp.337-340.
[124]L.Moura,N.Bj\,\#248,and rner,“Efficient E-Matching for SMT Solvers,”in Proceedings of the 21st international conference on Automated Deduction:Automated Deduction Bremen,Germany:Springer-Verlag,2007.
[125]B.Dutertre and L.de Moura,“A Fast Linear-Arithmetic Solver for DPLL(T),”in Computer Aided Verification,2006,pp.81-94.
[126]V.Ganesh and D.Dill,“A Decision Procedure for Bit-Vectors and Arrays,”in Computer Aided Verification,2007,pp.519-531.
[127]R.Brummayer and A.Biere,“Boolector:An Efficient SMT Solver for Bit-Vectors and Arrays,”in Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems:Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2009 York,UK:Springer-Verlag,2009.
[128]C.Barrett and C.Tinelli,“CVC3,”in Computer Aided Verification,2007,pp.298-302.
[129]M.Bofill,R.Nieuwenhuis,A.Oliveras,E.Rodriguez-Carbonell,and A.Rubio,“The Barcelogic SMT Solver,”in Computer Aided Verification,2008,pp.294-298.
[130]M.Bozzano,R.Bruttomesso,A.Cimatti,T.Junttila,P.Rossum,S.Schulz,and R.Sebastiani,“MathSAT:Tight Integration of SAT and Mathematical Decision Procedures,”J.Autom.Reason.,vol.35,pp.265-293,2005.
[131]R.Nieuwenhuis,A.Oliveras,and C.Tinelli,“Solving SAT and SAT Modulo Theories:From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T),”J.ACM,vol.53,pp.937-977,2006.
[132]H.Ganzinger,G Hagen,R.Nieuwenhuis,A.Oliveras,and C.Tinelli,“DPLL(T):Fast Decision Procedures,”in Computer Aided Verification,2004,pp.175-188.
[133]R.Nieuwenhuis and A.Oliveras,“DPLL(T)with Exhaustive Theory Propagation and Its Application to Difference Logic,”in Computer Aided Verification,2005,pp.321-334.
[134]D.Goldwasser,O.Strichman,and S.Fine,“A theory-based decision heuristic for DPLL(T),”in Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design Portland,Oregon:IEEE Press,2008.
[135]“Microsoft Phoenix Academic Program.”,http://research.microsoft.com/phoenix/.
[2]M.W.Eichin and J.A.Rochlis,“With microscope and tweezers:an analysis of the Internet virus of Nov.1988,”Proceedings of the IEEE Symp.Security and Privacy,1989.
[3]“Common Vulnerabilities and Exposures.”,http://cve.mitre.org.
[4]“Ph4nt0m Security Team.”,http://www.ph4nt0m.org
[5]R.Hastings and B.Joyce,“Purify:Fast detection of memory leaks and access errors.,”in Proceedings of the Winter USENIX Conference,1992.
[6]C.N.George,C.Jeremy,H.Matthew,M.Scott,and W.Westley,“CCured:type-safe retrofitting of legacy software,”ACM Trans.Program.Lang.Syst,vol.27,pp.477-526,2005.
[7]H.Etoh,“GCC Extension for Protecting Applications from Stack-smashing Attacks.,”2005,http://www.trl.ibm.com/projects/security/ssp/.
[8]W.Robertson,C.Kruegel,D.Mute,and F.Valeur,“Run-time Detection of Heap-based Overflows,”in Proceedings of the 17th USENIX conference on System administration San Diego,CA:USENIX Association,2003.
[9]D.Larochelle and D.Evans,“Statically detecting likely buffer overflow vulnerabilities,”in Proceedings of the 10th conference on USENIX Security Symposium-Volume 10 Washington,D.C.:USENIX Association,2001.
[10]N.Dor,M.Rodeh,and M.Sagiv,“CSSV:Towards a realistic tool for statically detecting all buffer overflows in C,”Acm Sigplan Notices,vol.38,pp.155-167,May 2003.
[11]D.Wagner,J.S.Foster,E.A.Brewer,and A.Aiken,“A First Step Towards Automated Detection of Buffer Overrun Vulnerabilities,”in Proceedings of the 2000 Network and Distributed Systems Security Conference San Diego,CA,2000.
[12]C.Flanagan,K.R.M.Leino,M.Lillibridge,G Nelson,J.B.Saxe,and R.Stata,“Extended static checking for Java,”in Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation Berlin,Germany:ACM,2002.
[13]K.Ashcraft and D.Engler,“Using Programmer-Written Compiler Extensions to Catch Security Holes,”in Proceedings of the 2002 IEEE Symposium on Security and Privacy:IEEE Computer Society,2002.
[14]X.Yichen and A.Alex,“Saturn:A scalable framework for error detection using Boolean satisfiability,”ACM Trans.Program.Lang.Syst,vol.29,p.16,2007.
[15]W.R.Bush,J.D.Pincus,and D.J.Sielaff,“A static analyzer for finding dynamic programming errors,”Softw.Pract.Exper.,vol.30,pp.775-802,2000.
[16]Y.Xie,A.Chou,and D.Engler,“ARCHER:using symbolic,path-sensitive analysis to detect memory access errors,”in Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering Helsinki,Finland:ACM,2003.
[17]P.Godefroid,N.Klarlund,and K.Sen,“DART:Directed automated random testing,”Acm Sigplan Notices,vol.40,pp.213-223,Jun 2005.
[18]K.Sen and G.Agha,“CUTE and jCUTE:Concolic unit testing and explicit path model-checking tools,”Computer Aided Verification,Proceedings,vol.4144,pp.419-423,2006.
[19]C.Cadar,V.Ganesh,P.M.Pawlowski,D.L.Dill,and D.R.Engler,“EXE:Automatically Generating Inputs of Death,”ACM Trans.Inf.Syst.Secur.,vol.12,pp.1-38,2008.
[20]C.Cristian,G Vijay,M.P.Peter,L.D.David,and R.E.Dawson,“EXE:automatically generating inputs of death,”in Proceedings of the 13th ACM conference on Computer and communications security Alexandria,Virginia,USA:ACM,2006.
[21]J.Yang,C.Sar,P.Twohey,C.Cadar,and D.Engler,“Automatically Generating Malicious Disks using Symbolic Execution,”in Proceedings of the 2006 IEEE Symposium on Security and Privacy:IEEE Computer Society,2006.
[22]P.Godefroid,“Compositional dynamic test generation,”in Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages Nice,France:ACM,2007.
[23]P.Godefroid,M.Y.Levin,and D.Molnar,“Automated Whitebox Fuzz Testing,”in Proceedings of NDSS'2008(Network and Distributed Systems Security)San Diego,2008,pp.151-166.
[24]C.Cadar,D.Dunbar,and D.Engler,“Klee:Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs,”in Operating System Design and Implementation(OSDI),2008.
[25]S.Anand,P.Godefroid,and N.Tillmann,“Demand-Driven Compositional Symbolic Execution,”in Tools and Algorithms for the Construction and Analysis of Systems,2008,pp.367-381.
[26]P.Godefroid,A.Kiezun,and M.Y.Levin,“Grammar-based whitebox fuzzing,”in Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation Tucson,AZ,USA:ACM,2008.
[27]A.V.Aho,R.Semi,and J.D.Ullman,Compilers:principles,techniques,and tools:Addison-Wesley Longman Publishing Co.,Inc.,1986.
[28]T.Fahringer,“Efficient Symbolic Analysis for Parallelizing Compilers and Performance Estimators,”J.Supercomput.,vol.12,pp.227-252,1998.
[29]M.R.Haghighat and C.D.Polychronopoulos,“Symbolic analysis for parallelizing compilers,”ACM Trans.Program.Lang.Syst,vol.18,pp.477-518,1996.
[30]M.P.Gerlek,E.Stoltz,and M.Wolfe,“Beyond induction variables:detecting and classifying sequences using a demand-driven SSA form,”ACM Trans.Program.Lang.Syst.,vol.17,pp.85-122,1995.
[31]M.R.Haghighat and C.D.Polychronopoulos,“Symbolic Program Analysis and Optimization for Parallelizing Compilers,”in Proceedings of the 5th International Workshop on Languages and Compilers for Parallel Computing:Springer-Verlag,1993.
[32]Z.Li,P.-C.Yew,and C.-Q.Zhu,“Data dependence analysis on multi-dimensional array references,”in Proceedings of the 3rd international conference on Supercomputing Crete,Greece:ACM,1989.
[33]R.Allen and K.Kennedy,Optimizing Compilers for Modern Architectures.San Fransisco,CA:Morgan Kaufmann,2002.
[34]S.Muchnick,Advanced Compiler Design and Implementation.San Fransisco,CA:Morgan Kaufmann,1997.
[35]U.BANERJEE,Dependence Analysis for Supercomputing.Boston:Kluwer,1988.
[36]M.BURKE and R.CYTRON,“Interprocedural dependence analysis and parallelization,”in proceedings of the Symposium on Compiler Construction 1986,pp.162-175.
[37]G.GOFF,K.KENNEDY,and C.-W.TSENG,“Practical dependence testing,”in proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI),Toronto,Ontario,Canada,1991,pp.15-29.
[38]D.KUCK,The Structure of Computers and Computations vol.1.New York:John Wiley and Sons,1987.
[39]D.E.MAYDAN,J.L.HENNESSY,and M.S.LAM,“Efficient and exact data dependence analysis,”in proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI),1991,pp.1-14.
[40]K.PSARRIS and K.KYRIAKOPOULOS,“Measuring the accuracy and efficiency of the data dependence tests,”in proceedings of the International Conference on Parallel and Distributed Computing Systems,2001.
[41]R.RUGINA and M.RINARD,“Symbolic bounds analysis of array indices,and accessed memory regions,”in proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation(PLDI),Vancouver,British Columbia,Canada,2000,pp.182-195.
[42]Z.SHEN,Z.LI,and P.C.YEW,“An empirical study on array subscripts and data dependencies,”in proceedings of the International Conference on Parallel Processing,1989,pp.145-152.
[43]M.WOLFE,High Performance Compilers for Parallel Computers.Redwood City,CA:Addison-Wesley,1996.
[44]H.ZIMA and B.CHAPMAN,Supercompilers for Parallel and Vector Computers.New York:ACM Press,1990.
[45]Z.Ammarguellat and I.W.L.Harrison,“Automatic recognition of induction variables and recurrence relations by abstract interpretation,”in Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation White Plains,New York,United States:ACM,1990.
[46]K.PSARRIS,“Program analysis techniques for transforming programs for parallel systems” Parallel Computing vol.28,pp.455-469,2003.
[47]K.Psarris and K.Kyriakopoulos,“The impact of data dependence analysis on compilation and program parallelization,”in Proceedings of the 17th annual international conference on Supercomputing San Francisco,CA,USA:ACM,2003.
[48]P.Wu,A.Cohen,J.Hoeflinger,and D.Padua,“Monotonic evolution:an alternative to induction variable substitution for dependence analysis,”in Proceedings of the 15th international conference on Supercomputing Sorrento,Italy:ACM,2001.
[49]R.A.v.Engelen,J.Birch,Y.Shou,B.Walsh,and K.A.Gallivan,“A unified framework for nonlinear dependence testing and symbolic analysis,”in Proceedings of the 18th annual international conference on Supercomputing Malo,France:ACM,2004.
[50]Y.Shou,R.A.v.Engelen,J.Birch,and K.A.Gallivan,“Toward efficient flow-sensitive induction variable analysis and dependence testing for loop optimization,”in Proceedings of the 44th annual Southeast regional conference Melbourne,Florida:ACM,2006.
[51]R.v.Engelen,“The CR# Algebra and its Application in Loop Analysis and Optimization,” Technical Report2004.
[52]E.V.Zima,“Recurrent Relations and Speed-up of Computations Using Computer Algebra Systems,”in Proceedings of the International Symposium on Design and Implementation of Symbolic Computation Systems:Springer-Verlag,1993.
[53]E.V.Zima,“On computational properties of chains of recurrences,”in Proceedings of the 2001 international symposium on Symbolic and algebraic computation London,Ontario,Canada:ACM,2001.
[54]O.Bachmann,“Chains of recurrences,”Kent State University,1997.
[55]O.Bachmann,P.S.Wang,and E.V.Zima,“Chains of recurrences:a method to expedite the evaluation of closed-form functions,”in Proceedings of the international symposium on Symbolic and algebraic computation Oxford,United Kingdom:ACM,1994.
[56]O.Bachmann,“MPCR:an efficient and flexible chains of recurrences server,”SIGSAM Bull.,vol.31,pp.15-21,1997.
[57]R.A.v.Engelen,J.Birch,and K.A.Gallivan,“Array Data Dependence Testing with the Chains of Recurrences Algebra,”in Proceedings of the Innovative Architecture for Future Generation High-Performance Processors and Systems:IEEE Computer Society,2004.
[58]J.L.Birch,“Methods for linear and nonlinear array data dependence analysis with the chains of recurrences algebra,”Florida State University,2007,p.233.
[59]V.Kislenkov,V.Mitrofanov,and E.Zima,“Multidimensional chains of recurrences,”in Proceedings of the 1998 international symposium on Symbolic and algebraic computation Rostock,Germany:ACM,1998.
[60]B.Beizer,Software Testing Techniques,2nd ed.New York:van Nostrand Reinhold,1990.
[61]H.Agrawal,J.R.Horgan,E.W.Krauser,and S.A.London,“Incremental regression testing,”in Software Maintenance,1993.CSM-93,Proceedings.,Conference on,1993,pp.348-357.
[62]Y.-F.Chen,D.S.Rosenblum,and K.-P.Vo,“TestTube:a system for selective regression testing,”in Proceedings of the 16th international conference on Software engineering Sorrento,Italy:IEEE Computer Society Press,1994.
[63]E.Engstr\,\#246,M.Skoglund,and P.Runeson,“Empirical evaluations of regression test selection techniques:a systematic review,”in Proceedings of the Second ACM-IEEE international symposium on Empirical software engineering and measurement Kaiserslautern,Germany:ACM,2008.
[64]P.K.Chittimalli and M.J.Harrold,“Regression test selection on system requirements,”in Proceedings of the 1st conference on India software engineering conference Hyderabad,India:ACM,2008.
[65]G.Rothermel,S.Elbaum,A.G.Malishevsky,P.Kallakuri,and X.Qiu,“On test suite composition and cost-effective regression testing,”ACM Trans.Softw.Eng.Methodol.,vol.13,pp.277-331,2004.
[66]M.J.Harrold,J.A.Jones,T.Li,D.Liang,A.Orso,M.Pennings,S.Sinha,S.A.Spoon,and A.Gujarathi,“Regression test selection for Java software,”in Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming,systems,languages,and applications Tampa Bay,FL,USA:ACM,2001.
[67]T.L.Graves,M.J.Harrold,J.-M.Kim,A.Porter,and G.Rothermel,“An empirical study of regression test selection techniques,”ACM Trans.Softw.Eng.Methodol.,vol.10,pp.184-208,2001.
[68]J.Bible,G.Rothermel,and D.S.Rosenblum,“A comparative study of coarse-and fine-grained safe regression test-selection techniques,”ACM Trans.Softw.Eng.Methodol.,vol.10,pp.149-183,2001.
[69]F.I.Vokolos and P.G Frankl,“Empirical evaluation of the textual differencing regression testing technique,”in Software Maintenance,1998.Proceedings.International Conference on,1998,pp.44-53.
[70]R.Gregg and H.Mary Jean,“A safe,efficient regression test selection technique,”ACM Trans.Softw.Eng.Methodol.,vol.6,pp.173-210,1997.
[71]D.Jeffrey and N.Gupta,“Experiments with test case prioritization using relevant slices,”J.Syst.Softw.,vol.81,pp.196-221,2008.
[72]K.K.Aggrawal,Y.Singh,and A.Kaur,“Code coverage based technique for prioritizing test cases for regression testing,”SIGSOFT Softw.Eng.Notes,vol.29,pp.1-4,2004.
[73]A.Srivastava and J.Thiagarajan,“Effectively prioritizing tests in development environment,”in Proceedings of the 2002 ACM SIGSOFT international symposium on Software testing and analysis Roma,Italy:ACM,2002.
[74]S.Elbaum,A.G Malishevsky,and G Rothermel,“Prioritizing test cases for regression testing,”in Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis Portland,Oregon,United States:ACM,2000.
[75]H.Zhong,L.Zhang,and H.Mei,“An experimental study of four typical test suite reduction techniques,”Inf.Softw.Technol.,vol.50,pp.534-546,2008.
[76]Y.Chen,R.L.Probert,and H.Ural,“Regression test suite reduction using extended dependence analysis,”in Fourth international workshop on Software quality assurance:in conjunction with the 6th ESEC/FSE joint meeting Dubrovnik,Croatia:ACM,2007.
[77]W.E.Wong,J.R.Horgan,S.London,and A.P.Mathur,“Effect of test set minimization on fault detection effectiveness,”Softw.Pract.Exper.,vol.28,pp.347-369,1998.
[78]R.Gregg,H.M.Jean,O.Jeffery,and H.Christine,“An Empirical Study of the Effects of Minimization on the Fault Detection capabilities of Test Suites,”Oregon State University1998.
[79]M.J.Harrold,R.Gupta,and M.L.Soffa,“A methodology for controlling the size of a test suite,”ACM Trans.Softw.Eng.Methodol.,vol.2,pp.270-285,1993.
[80]J.W.Hunt and M.D.Mcllroy,“An Algorithm for Differential File Comparison,”Bell Laboratories 1976.
[81]J.I.Maletic and M.L.Collard,“Supporting Source Code Difference Analysis,”in Proceedings of the 20th IEEE International Conference on Software Maintenance:IEEE Computer Society,2004.
[82]R.Cytron,J.Ferrante,B.K.Rosen,M.N.Wegman,and F.K.Zadeck,“An efficient method of computing static single assignment form,”in Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages Austin,Texas,United States:ACM,1989.
[83]R.Kennedy,S.Chan,S.-M.Liu,R.Lo,P.Tu,and F.Chow,“Partial redundancy elimination in SSA form,”ACM Trans.Program.Lang.Syst,vol.21,pp.627-676,1999.
[84]M.M.Brandis and H.Mossenbock,“Single-pass generation of static single-assignment form for structured languages,”ACM Trans.Program.Lang.Syst,vol.16,pp.1684-1698,1994.
[85]H.Srinivasan,J.Hook,and M.Wolfe,“Static single assignment for explicitly parallel programs,”in Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages Charleston,South Carolina,United States:ACM,1993.
[86]C.McConnell and R.E.Johnson,“Using static single assignment form in a code optimizer,” ACM Lett.Program.Lang.Syst.,vol.1,pp.152-160,1992.
[87]R.Cytron,J.Ferrante,B.K.Rosen,M.N.Wegman,and F.K.Zadeck,“Efficiently computing static single assignment form and the control dependence graph,”ACM Trans.Program.Lang.Syst.,vol.13,pp.451-490,1991.
[88]P.Briggs,K.D.Cooper,and L.Torczon,“Rematerialization,”in Proceedings of the ACM SIGPLAN 1992 conference on Programming language design and implementation San Francisco,California,United States:ACM,1992.
[89]M.N.Wegman and F.K.Zadeck,“Constant propagation with conditional branches,”ACM Trans.Program.Lang.Syst,vol.13,pp.181-210,1991.
[90]F.Jeanne,J.O.Karl,and D.W.Joe,“The program dependence graph and its use in optimization,”ACM Trans.Program.Lang.Syst.,vol.9,pp.319-349,1987.
[91]T.Y.Chen and Y.Y.Cheung,“Structural Properties of Post-Dominator Trees,”in Proceedings of the Australian Software Engineering Conference:IEEE Computer Society,1997.
[92]V.C.Sreedhar,G R.Gao,and Y.-f.Lee,“Incremental computation of dominator trees,”in Papers from the 1995 ACM SIGPLAN workshop on Intermediate representations San Francisco,California,United States:ACM,1995.
[93]G.Ramalingam and T.Reps,“An incremental algorithm for maintaining the dominator tree of a reducible flowgraph,”in Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages Portland,Oregon,United States:ACM,1994.
[94]B.D.Sutter,L.V.Put,and K.D.Bosschere,“A practical interprocedural dominance algorithm,”ACM Trans.Program.Lang.Syst,vol.29,p.19,2007.
[95]S.Horwitz and T.Reps,“The Use Of Program Dependence Graphs In Software Engineering,”in Software Engineering,1992.International Conference on,1992,pp.392-411.
[96]K.B.Gallagher,“Some notes on interprocedural program slicing,”in Source Code Analysis and Manipulation,2004.Fourth IEEE International Workshop on,2004,pp.36-42.
[97]R.Gopal,“Dynamic program slicing based on dependence relations,”in Software Maintenance,1991.,Proceedings.Conference on,1991,pp.191-200.
[98]R.Johnson and K.Pingali,“Dependence-based program analysis,”in Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation Albuquerque,New Mexico,United States:ACM,1993.
[99]G.Ramalingam,“On loops,dominators,and dominance frontiers,”ACM Trans.Program.Lang.Syst,vol.24,pp.455-490,2002.
[100]G.Ramalingam,“On loops,dominators,and dominance frontier,”SIGPLAN Not.,vol.35,pp.233-241,2000.
[101]L.Heng,W.K.Chan,and T.H.Tse,“Static Slicing for Pervasive Programs,”in Quality Software,2006.QSIC 2006.Sixth International Conference on,2006,pp.185-192.
[102]Z.Yingzhou,X.Baowen,and J.E.Labra Gayo,“A formal method for program slicing,”in Software Engineering Conference,2005.Proceedings.2005 Australian,2005,pp.140-148.
[103]D.Binkley,S.Danicic,T.Gyimothy,M.A.H.M.Harman,A.A.K.A.Kiss,and B.A.K.B.Korel,“Minimal slicing and the relationships between forms of slicing,”in Source Code Analysis and Manipulation,2005.Fifth IEEE International Workshop on,2005,pp.45-54.
[104]F.Umemori,K.Konda,R.Yokomori,and K.A.I.K.Inoue,“Design and implementation of bytecode-based Java slicing system,”in Source Code Analysis and Manipulation,2003.Proceedings.Third IEEE International Workshop on,2003,pp.108-117.
[105]A.R.Kulkarni and S.Ramesh,“Static slicing of reactive programs,”in Source Code Analysis and Manipulation,2003.Proceedings.Third IEEE International Workshop on,2003,pp.98-107.
[106]J.Rilling and B.Karanth,“A hybrid program slicing framework,”in Source Code Analysis and Manipulation,2001.Proceedings.First IEEE International Workshop on,2001,pp.12-23.
[107]P.Kilpatrick,D.Crookes,and M.Owens,“Program slicing:a computer aided programming technique,”in Software Engineering,1988 Software Engineering 88.,Second IEE/BCS Conference:,1988,pp.60-64.
[108]J.C.Hwang,M.W.Du,and C.R.Chou,“The influence of language semantics on program slices,”in Computer Languages,1988.Proceedings.,International Conference on,1988,pp.120-127.
[109]E.V.Zima,“Automatic construction of systems of recurrence relations,”USSR Computational Mathematics and Mathematical Physics,pp.193-197,1986.
[110]E.V.Zima,“Simplification and optimization transformations of chains of recurrences,”in proceedings of the International Symposium on Symbolic and Algebraic Computing,Montreal,Canada,1995.
[111]R.v.Engelen,“Efficient Symbolic Analysis for Optimizing Compilers,”in proceedings of the ETAPS International Conference on Compiler Construction(CC),2001,pp.118-132.
[112]R.v.Engelen,“Symbolic Evaluation of Chains of Recurrences for Loop Optimization,” Technical Report TR-000102,2000.
[113]Y.Shou,R.Engelen,and J.Birch,“Flow-Sensitive Loop-Variant Variable Classification in Linear Time,”in Languages and Compilers for Parallel Computing:20th International Workshop,LCPC 2007,Urbana,IL,USA,October 11-13,2007,Revised Selected Papers:Springer-Verlag,2008,pp.323-337.
[114]J.Birch,R.A.v.Engelen,K.A.Gallivan,and Y.Shou,“An empirical evaluation of chains of recurrences for array dependence testing,”in Proceedings of the 15th international conference on Parallel architectures and compilation techniques Seattle,Washington,USA:ACM,2006.
[115]D.Detlefs,G.Nelson,and J.B.Saxe,“Simplify:a theorem prover for program checking,”J.ACM,vol.52,pp.365-473,2005.
[116]T.Ball,B.Cook,S.K.Lahiri,and L.Zhang,“Zapato:Automatic Theorem Proving for Predicate Abstraction Refinement,”in Computer Aided Verification,2004,pp.457-461.
[117]J.P.Marques-Silva and K.A.Sakallah,“GRASP:a search algorithm for propositional satisfiability,”Computers,IEEE Transactions on,vol.48,pp.506-521,1999.
[118]H.Zhang,“SATO:An efficient prepositional prover,”in Automated Deduction—CADE-14,1997,pp.272-275.
[119]M.W.Moskewicz,C.F.Madigan,Y.Zhao,L.Zhang,and S.Malik,“Chaff:engineering an efficient SAT solver,”in Design Automation Conference,2001.Proceedings,2001,pp.530-535.
[120]S.A.Cook,“The complexity of theorem-proving procedures,”in Proceedings of the third annual ACM symposium on Theory of computing Shaker Heights,Ohio,United States:ACM,1971.
[121]K.R.Apt,“Some Remarks on Boolean Constraint Propagation,”in Selected papers from the Joint ERCIM/Compulog Net Workshop on New Trends in Contraints:Springer-Verlag,2000.
[122]L.Shuvendu and Q.Shaz,“Back to the future:revisiting precise program verification using SMT solvers,”in Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages San Francisco,California,USA:ACM,2008.
[123]L.de Moura and N.Bjwner,“Z3:An Efficient SMT Solver,”in Tools and Algorithms for the Construction and Analysis of Systems,2008,pp.337-340.
[124]L.Moura,N.Bj\,\#248,and rner,“Efficient E-Matching for SMT Solvers,”in Proceedings of the 21st international conference on Automated Deduction:Automated Deduction Bremen,Germany:Springer-Verlag,2007.
[125]B.Dutertre and L.de Moura,“A Fast Linear-Arithmetic Solver for DPLL(T),”in Computer Aided Verification,2006,pp.81-94.
[126]V.Ganesh and D.Dill,“A Decision Procedure for Bit-Vectors and Arrays,”in Computer Aided Verification,2007,pp.519-531.
[127]R.Brummayer and A.Biere,“Boolector:An Efficient SMT Solver for Bit-Vectors and Arrays,”in Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems:Held as Part of the Joint European Conferences on Theory and Practice of Software,ETAPS 2009 York,UK:Springer-Verlag,2009.
[128]C.Barrett and C.Tinelli,“CVC3,”in Computer Aided Verification,2007,pp.298-302.
[129]M.Bofill,R.Nieuwenhuis,A.Oliveras,E.Rodriguez-Carbonell,and A.Rubio,“The Barcelogic SMT Solver,”in Computer Aided Verification,2008,pp.294-298.
[130]M.Bozzano,R.Bruttomesso,A.Cimatti,T.Junttila,P.Rossum,S.Schulz,and R.Sebastiani,“MathSAT:Tight Integration of SAT and Mathematical Decision Procedures,”J.Autom.Reason.,vol.35,pp.265-293,2005.
[131]R.Nieuwenhuis,A.Oliveras,and C.Tinelli,“Solving SAT and SAT Modulo Theories:From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T),”J.ACM,vol.53,pp.937-977,2006.
[132]H.Ganzinger,G Hagen,R.Nieuwenhuis,A.Oliveras,and C.Tinelli,“DPLL(T):Fast Decision Procedures,”in Computer Aided Verification,2004,pp.175-188.
[133]R.Nieuwenhuis and A.Oliveras,“DPLL(T)with Exhaustive Theory Propagation and Its Application to Difference Logic,”in Computer Aided Verification,2005,pp.321-334.
[134]D.Goldwasser,O.Strichman,and S.Fine,“A theory-based decision heuristic for DPLL(T),”in Proceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design Portland,Oregon:IEEE Press,2008.
[135]“Microsoft Phoenix Academic Program.”,http://research.microsoft.com/phoenix/.