基于CEGAR的C程序空指针解引用检测

段　钊　田　聪　段振华

(西安电子科技大学计算机理论与技术研究所　西安　710071)

(ctian@mail.xidian.edu.cn)



基于CEGAR的C程序空指针解引用检测

段钊田聪段振华

(西安电子科技大学计算机理论与技术研究所西安710071)

(ctian@mail.xidian.edu.cn)

CEGAR Based Null-Pointer Dereference Checking in C Programs

Duan Zhao, Tian Cong, and Duan Zhenhua

(InstituteofComputingTheoryandTechnology,XidianUniversity,Xi’an710071)

AbstractWith the rapid growth of computer software in both scale and complexity, more and more attention has been paid by software developers on the reliability and security issue. Null-pointer dereference is a kind of errors which often occur in programs.This paper proposes a CEGAR based null-pointer dereference verification approach for C programs. With this method, first, a linear temporal logic (LTL) formula is used to specify the null-pointer dereference problem. Then whether null-pointer dereference occuring in a program is checked by a CEGAR based model checking approach. In order to verify null-pointer dereference problem in a total automatic way, this paper also studies how to generate temporal logic formulas automatically with respective to null-pointer dereference problem. Experimental results show that the proposed approach is useful in practice for checking null-pointer dereference in C programs with large scale.

Key wordsmodel checking; abstraction refinement; null-pointer dereference; program verification; temporal logic

摘要随着计算机软件规模和复杂度的日益增长，软件系统的可靠性和安全性倍受关注.空指针解引用是程序中常见的一类错误.提出了一种基于反例制导抽象精化CEGAR的C程序空指针解引用检测方法.该方法首先使用线性时序逻辑描述空指针解引用问题，然后通过抽象精化的方法检测待测程序中是否含有空指针解引用错误.为了达到完全自动验证的目标，同时针对空指针解引用问题，研究了该类性质的时序逻辑表达方法，并自动从程序中针对所有的指针变量，形成相应的时序逻辑公式.实验结果表明，所提出的方法在大规模C程序的空指针解引用检测方面有着重要的实际应用价值.

关键词模型检测；抽象精化；空指针解引用；程序验证；时序逻辑

计算机软件已深入到国防建设和国计民生的各个领域，如航天航空、工业控制、交通、医疗、教育和社交等，成为当今社会不可或缺的一部分.面对多样化的需求，软件的规模和复杂性不断增大，因而软件的可靠性和安全性更加难以得到保障.目前，大部分软件系统都存在各种各样的错误和缺陷.有的软件虽然可以正常运行，但是其内部仍然存在许多错误隐患,在特定情况下会导致软件性能下降，甚至引起程序崩溃，从而造成巨大的损失.为了提高软件的可信性，研究人员提出大量的技术来检测和预防软件中的错误和缺陷.

C程序中指针的使用十分广泛，而且语法灵活，但易错.由于指针而引发的内存错误往往难以追踪和分析,空指针解引用是其中常见的错误之一.如果一个指针表达式指向NULL，或者未被初始化，或者指向一个已被释放的内存，那么，使用该表达式的解引用就会导致系统崩溃或者得到错误的数据.

许多查找软件错误的技术被提出.其中，静态分析是在不执行程序的情况下通过直接分析源程序来检查程序中的错误,主要包括路径敏感不敏感分析方法[1]和流敏感不敏感分析方法[2-3]等.程序测试[4-5]是对程序的每一个模块在使用前进行测试，保证该模块的正确性.定理证明[6]将待测问题转化为可满足性问题，通过判断命题逻辑公式的可满足性来检测程序中是否存在错误.模型检测[7-8]主要是把待检测程序描述为状态迁移系统，把待检测的问题用时序逻辑公式表示出来，然后检测状态迁移系统是否满足性质.近年来，许多研究将模型检测、定理证明和静态分析等技术相结合，利用各种方法的优势来检测程序中的错误.

在空指针解引用方面，Dirk等人开发的自动验证工具BLAST[9-11]，可以验证C程序中的安全性质.Dirk等人将他们的方法进行了扩展，开发了新的工具CPAChecker[12-13].但是使用BLAST和CPAChecker检测程序中的空指针解引用需要预先在程序中插桩，如何完全自动地插桩是一个有待解决的实际问题.CMBC[14]是Edmund等人开发的一种限界模型检测工具.Charatonik等学者在此工具的基础上，通过限界的思想来检测程序中是否存在空指针解引用问题[15].另外，还有一些研究针对并行程序中空指针解引用问题[16].在国内，也有一些学者从事这方面的研究，如文献[17]给出了一种检测C程序中基于区域内存模型的空指针解引用错误的方法.

总之，现有的程序模型检测方法和工具很多，它们主要是通过对源程序进行插桩，然后再分析插桩后的程序.CBMC和BLAST支持对程序的自动插桩；但是，它们是对程序中每个指针的每一次解引用都进行插桩，因而会大大增加源程序的代码量.CPAChecker则需要手动地进行插桩,如果给每个位置插桩，同样会增加代码量.

本文提出了一种基于反例制导抽象精化(counter example-guided abstraction refinement, CEGAR)[18]的C程序空指针解引用检测方法.该方法首先使用线性时序逻辑(linear temporal logic, LTL)描述空指针解引用问题，然后通过抽象精化的方法检测待测程序中是否含有空指针解引用错误.为了达到完全自动验证的目标，本文同时针对空指针解引用问题，研究了该类性质的时序逻辑表达方法，并自动从程序中针对所有的指针变量形成相应的时序逻辑公式.实验结果表明，该方法可以自动地对程序中的所有指针进行检测，错误覆盖率高，对大规模程序的检测有着很好的实际应用价值.

1空指针解引用问题的LTL描述

1.1LTL

模型检测中，一般使用时序逻辑公式描述待验证的性质.本文使用LTL来描述空指针解引用问题.

设AP是原子命题集合，LTL公式是由AP中的元素和操作符组成.其中，操作符包括逻辑非()、逻辑与(∧)、next(○)、until(∪)和release(R).LTL的语法定义如下:

φ∷=p|ψ|φ∧ψ|○ψ|φ∪ψ|φRψ,p∈AP.

LTL公式的语义解释在线性结构上.一个线性结构是一个无限序列x=x(0)，x(1)，….其中，x(i)是AP到{true, false}的映射.一个LTL公式φ在线性结构x的第i个位置满足一个线性结构x，记作:x,i⟹φ.语义定义如下:

x,i⟹p,如果x(i)(p)=true,p∈AP;

x,i⟹ψ,如果x,i⟹ψ;

x,i⟹φ∨ψ,如果x,i⟹φ或x,i⟹ψ;

x,i⟹○φ,如果x,i+1⟹φ;

x,i⟹φ∪ψ,如果存在j≥i,使得对于任意的

i′∈{i,i+1,…,j-1},x,i′⟹φ,并且x,j⟹ψ;

x,i⟹φRψ,如果对所有的j≥i,x,j⟹ψ,

或者存在j≥i,使得对于任意的

i′∈{i,i+1,…,j-1},x,i′⟹ψ,并且x,j⟹φ.

其它附加的逻辑操作符定义如下:

另外，时序操作符sometimes(◇)和always(□)的定义如下：

LTL公式可以表示为范式.对于一个LTL公式φ,它的范式定义为

其中，βi是状态公式，即只包含逻辑操作符的公式;φi是一个任意的主操作符不为析取操作的LTL公式.在范式中，每一个析取项都代表一个迁移关系.直观地讲，范式表示存在一个整数i，βi在当前状态可满足，φi在下一状态可满足.已证明，所有的LTL公式都可以等价地转化为它的范式[19].

1.2LTL到TGBA的转换

任何一个LTL公式可以被等价地转换为一个基于迁移的广义Büchi自动机(transition based generalized Büchi automata, TGBA)[20].为了构造LTL公式φ的TGBA，首先创建初始状态[φ]，然后将φ转换为范式.假设:

φ≡(p∧r∧p∧r)∧○(φ1∧φ2)∨

p∧r∧○φ3∨p∧r∧○(φ4∧φ5),

那么可以生成3个新结点，即[φ1∧φ2]，[φ3]和[φ4∧φ5]，如图1所示:

Fig. 1　Constructing TGBA.图1　构造TGBA

同时，生成迁移关系为

为了完成整个TGBA的构造，需要针对每个新生成的结点，通过将表示该结点的公式转换成范式，从而不断地产生新的结点，直到没有新的结点可以被生成.这样的一个图我们称为φ的范式图.

在此过程中，必须考虑一个问题：对于形如p∪q的公式，q最终要发生，即q不能被无限地延迟.但是，在范式图中没有显式地体现出q有没有发生.

因此，为了准确地刻画∪操作的语义，本文进一步在范式图的边上增加Flag集合标记.我们关注公式中不同的∪操作.对于每一个主操作符为∪的子式，使用一个唯一整数下标i来区分，这里i>0.这样，第i个∪操作，记为∪i.一个LTL公式的范式图中，一个状态[φ]中的所有主操作符为∪的子式所对应的下标构成的整数集合称为Untilφ.整个范式图中，所有主操作符为∪的子式所对应的下标构成的整数集合称为AllUntil.据此，指向状态[φ]的迁移上的标记为Flag=AllUntilUntilφ.

对于一个LTL公式φ=p∪(q∪r)，它对应的TGBA如图2所示，在图2中“{}”是每一个状态所包含的主操作符为∪的子式的整数标记集合,“[]”是每一条迁移上的Flag集合.

Fig. 2　TGBA of the formula φ.图2　公式φ的TGBA.

从图2可以看出，“q∪r”，记为φ中的主操作符∪,被标记为4；“p∪(q∪r)”，记为φ1中的主操作符∪,被标记为5；“true”，记为φ2，不包含∪.所以，整个TGBA的AllUntil集合为{4,5}，Untilφ为{4}，Untilφ1为{5}，Untilφ2为{}.

范式图以及Flag标记构成了与给定LTL公式等价的TGBA.TGBA上一个无穷路径是指从初始结点出发的一个结点与边相交互的无穷序列，π=n0,e0,n1,e1,…,(ni,ei,…,nj,ej)ω,0≤i≤j.为了方便，我们用infn(π)表示π的循环部分的结点集合，infe(π)表示循环部分的边集合.一个路径π是可接收的，当且仅当：

AllUntil={Flag(e)|e∈infe(e)}.

1.3空指针解引用的LTL描述

空指针解引用问题指：当程序中使用某个指针变量的解引用形式时，该指针变量为空.在该情况下会导致程序出错甚至崩溃.为了使用LTL公式表示空指针解引用问题，我们首先定义2个命题:

命题1.d:表示指针p≠null.d为真当且仅当在当前状态下指针变量p≠null.

命题2.r:表示使用了指针p的解引用形式，即*p或p→.r为真当且仅当当前状态使用了指针的解引用形式.

因此，指针变量p的空指针解引用可以描述为：程序中某一时刻p=null且出现了对p的解引用形式.在模型检测中，一般描述期望的性质：即该程序中不存在空指针解引用.该期望的性质用LTL公式描述为□(r→d).

为了检测待测程序是否满足性质□(r→d)，理论上我们需要将□(r→d)的否定，即(□(r→d))转换为TGBA;然后检测程序中是否存在可能的执行路径与所得到的TGBA的接收路径相吻合.

Fig. 3　TGBA of formula true∪(d∧ r).图3　公式true∪(d∧ r)的TGBA

TransitionpredecessoredgesuccessorFlagtrue∪(d∧r)d∧rtrue{1}true∪(d∧r)truetrue∪(d∧r){}truetruetrue{1}

2空指针解引用性质的LTL公式生成

如1.3节所述，程序中不存在空指针解引用的性质可以通过LTL公式□(r→d)来描述.因此，我们可以看出，对于不同的指针变量公式是不变的.但是命题d和r的具体定义不同，它们要对应具体的指针变量.因此，基于这种模式，本节给出了针对任意指针变量的LTL公式形式方法.

在程序中，指针变量的定义存在2种情况：1) 声明语句，可以以全局或局部变量的形式出现；2) 函数的形参，出现在函数的定义中.为了对所有的指针变量形成相应的LTL公式，我们首先通过分析程序的语法树，提取所有的指针变量，并记录相关的变量名称、类型和作用域(通过所在函数的名称来体现，其中全局变量略去函数名称)；然后针对不同的指针变量，例如变量v，定义命题d和r：

具体的指针变量的提取算法如算法1所示：

算法1. 指针变量的提取.

输入：控制流自动机cfa、保存变量信息的集合varInfo、保存函数信息的集合funcInfo、保存类型信息的集合typeInfo；

输出:varInfo.

① fornodeincfado*对cfa中每一个结点*

② ifnode是函数入口结点then*提取函

③paras=extractFuncInfo(node,

funcInfo);

④ forparainparasdo

⑤ ifpara是一个指针变量then

⑥extractVarInfo(para,varInfo);

⑦ end if

⑧ end for

⑨ end if

⑩edges=getLeavingEdges(node);

在算法1中，为了方便分析，提取指针变量时，同时记录了所在函数和复杂类型的信息.在得到所有变量信息后，可以任意选择一个变量，生成对应的LTL公式进行检测,也可以选择对所有变量自动地逐个形成公式并检测.

3基于CEGAR的空指针解引用模型检测

本节首先描述了模型检测中使用的2种数据结构：控制流自动机(control flow antomata, CFA)和抽象可达图(abstract reachability graph, ARG);然后，详细地介绍了基于CEGAR的空指针解引用模型检测方法.

3.1CFA和ARG

CFA是一个有向图.其中，结点代表程序的位置，通过一个程序计数器的值来编号;边表示的是连接2个结点的操作，对应C程序的语句，包括赋值操作、分支语句、函数调用和return语句等.

一个程序的CFA可以定义为一个四元组A={L,O,lentry,lexit}，其中，L是程序位置的集合;O⊆L×ops×L是控制流边的结合，表示控制流2个相邻结点之间执行的操作;lentry∈L是程序的起始位置;lexit∈L是程序的终止位置.

对于CFA中的一个程序位置l∈L，l的前驱集合定义为Pre(l)={l′|(l′,ops,l)∈O},l的后继集合定义为Succ(l)={l′|(l,ops,l′)∈O}.以下面代码为例，它的CFA如图4所示.

① void main(){

② inti;

③ int*p;

④ ifi<2

⑤p=&i;

⑥ end if

⑦*p=1;

⑧ }

Fig. 4　CFA.图4　控制流自动机

ARG是在考虑CFA中每个位置的谓词真值的情况下，通过展开CFA而得到的.它表示的是程序可达的状态空间.

给定一个程序的控制流图A={L,O,lentry,lexit}和相关的谓词集合Pred.该程序的ARG为一个四元组G={N,E,Ninit,Nf}.其中，N是结点集合，对于任意的n∈N，n=(l,Pred(l)),l∈L，Pred：L→2Pred称为可达域，表示位置l与Pred的映射关系;E⊆N×ops×N是控制流边的子集;Ninit和Nf是初始结点集合和终止结点集合.

为了方便，对于一个结点n=(l,Pred(l))∈N，我们用n.l表示l;用n.r表示Pred(l).如果n∈Ninit(Nf),则n.l=lentry(lexit).

实际上，ARG是程序的抽象模型，其中一条路径对应于程序的一次执行.一个结点n的可达域(n.r)表示假设程序沿着一个操作序列执行，从起始结点到结点n得到的可达状态的近似集合.因此，考虑的谓词越少，ARG就越小，验证的效率越高.一个CFA可以看成一个特殊的ARG，其中，所有结点的可达域都为空.但是在ARG中，一条不满足期望性质的路径可能在实际程序中不存在.然而，基于CEGAR的懒惰抽象(lazy abstraction)[21]方法可以通过插值得到更多的谓词，从而有效地消除虚假反例.

3.2基于CEGAR的C程序空指针解引用检测

Fig. 5　Framework of CEGAR based model checking.图5　基于CEGAR的模型检测整体框架

基于CEGAR的C程序空指针解引用模型检测的整体框架如图5所示.1)使用LTL公式P描述期望的性质，即程序中不存在空指针解引用问题;2)检测程序是否可以满足P的否定.如果可以满足，那么程序中存在可能的执行路径与期望的性质相违背，否则程序满足期望的性质.程序的状态空间往往非常大，甚至无穷大，因此，本文使用谓词抽象的方法得到程序的一个抽象模型.在初始的抽象模型中，仅关心与性质P相关的所有谓词.如图5所示，通过抽象我们从待测程序Pro得到它的抽象模型M′;然后检测M′是否可以满足性质的否定，即P.若M′的所有路径都不能满足P，可以给出结论：程序Pro中没有空指针解引用发生;反之，如果在M′中找到一条路径可以满足P，需要进一步检测该路径的真实性，即该路径是否在源程序中存在.若该路径是真实存在的路径，那么我们找到了程序中的一个空指针解引用错误;否则，如果该路径是虚假的，需要进一步通过添加新的谓词来对M′进行细化.重复以上过程，直到发现一个错误，或者证明程序中没有错误为止.在CPAChecker的CEGAR算法中，细化操作是通过调用SMT求解器来完成的,它将一条反例路径转化为SMT求解器可处理的公式序列，然后通过求解器来求解.新的谓词是通过Craig差值[22]算法得到的.

本文的算法是在现有的软件模型检测工具CPAChecker的基础上实现.CPAChecker自身不能支持时序逻辑性质的检测,它需要首先在程序中对待检测的问题进行插桩，然后使用上述CEGAR循环进行检测.通过插桩的方式，只需要对能到达插桩的位置的路径进行检测，从这个角度看，插桩的方法隐式地缩小检测范围，在一定程度上对检测路径进行了筛选，而且，如果程序中有错误，那么错误肯定在插桩的位置，方便定位错误.CEGAR算法检测流程图如图6所示.在图6中，首先读入插桩后的C程序，并生成程序的CFA;然后根据插桩信息，展开CFA，提取谓词，生成ARG.如果错误标签不可达，即不存在反例路径(counterexample, CE)，说明程序安全；否则需判断反例路径是否虚假.如果反例路径是虚假的，说明考虑的谓词太少，需要提取新的谓词进一步细化，然后继续检测;如果反例路径不是虚假的，则说明程序不安全，输出反例路径.

Fig. 6　Flow diagram of the CEGAR algorithm in CPAChecker.图6　CPAChecker中CEGAR算法的流程图

3.3on-the-fly检测

为了缓解验证过程中的状态空间，本文结合CFA和LTL性质，采用on-the-fly的方式逐步生成ARG，同时对性质进行检测.

算法2.LTLModelCheck(M,V).

输入：带验证的程序M、待检测的指针变量V；

输出：true或false.

①target=null,success=false;

②M→cfa;*生成CFA*

③AP=generate(V),P=Property(AP);

④S0=initARGState(cfa,AP,P);*初始状态*

⑤reached={S0};*可达状态集合*

⑥waitlist={S0};*一个栈，存放未处理的状态*

⑦AllUntil=LTL2NF(P);

⑧ do{

⑨target=generateARG(cfa,reached,

waitlist,AllUntil);

⑩ iftarget!=null then

算法3.generateARG(cfa,reached,waitlist,AllUntil).

输入：控制流自动机cfa、可达状态集合reached、用来存放未处理状态的一个栈waitlist、待验证性质对应的AlLUntil集合AllUntil;

输出：1个ARGState.

① whilewaitlist!=null do

②s=getTopWaitlist(),p=P(s);

③TR=nextStateNF(s,p);

④ ifTR=null then goto ③;

⑤ forT′ inTRdo

⑥sucs=computeSucs(s,cfa) ;*后继状

⑦ ifsucs==null then

⑧ ifexistCE(reached,s,AllUntil) then

⑨ returns;

⑩ end if

then

在算法3中,语句p=P(s)计算状态s的性质集合；函数stop判断后继状态suc是否被覆盖；函数getSucProperty计算后继状态满足的性质；函数CP计算后继状态需要满足的命题；函数existCE判断是否存在反例路径.函数getSucProperty的计算过程如算法4所示.

算法4.getSucProperty(S,T).

输入：1个ARG状态S、性质的1条迁移T；

输出：S的后继状态满足的性质.

①M=S.getPropositions();*状态S满足的命题集合*

②booleanbool=true;

④ forminMdo*对M中每一个命题*

⑤ ifm∧ε′ !=false then

⑥ continue;

⑦ else

⑧bool=false;

⑨ break;

⑩ end if

算法4中，T为迁移关系,ε′代表的是迁移关系T的接受条件.如果命题集合M中的每一个命题与ε′的交集都不为空，则说明状态S满足性质P′.

函数CP的计算方法如下：1) 求出初始状态到S的路径，记作path.2)将path转为SMT能够接受的形式，记作pathformula.3)得到前驱状态的命题集合pp.4) 对集合pp中的命题d，做如下操作：将命题d转为SMT公式f，加入pathformula，并用SMT求解.如果结果为true，则说明S状态满足命题d；否则，S状态不满足命题d，即满足d的否定.对于命题r，则通过分析对应的c表达式来判断其是否可满足.

函数existCE的计算过程如算法5所示.其中，path为从初始状态到达输入状态E的路径.反例路径是根据path的循环部分来判断.

算法5.existCE(reached,E,AllUntil).

输入：可达状态集合reached、一个ARG状态E、待验证性质对应的AlLUntil集合AllUntil；

输出：true或false.

①path=getPath(reached,E);

② foreinpathdo

③Flag=getFlag(e);*计算Flag集合*

④ foriinFlagdo

⑤Fi=Fi∪{e};

⑥ end for

⑦ end for

⑧ foriinAllUntildo

⑨ ifFi∧path!=null then

⑩ continue;

4实验结果分析

为了验证本文提出的方法，我们在CPAChecker的基础上开发了C程序空指针解引用检测工具NULPChecker，并通过程序验证Benchmark程序*https:svn.sosy-lab.orgsoftwaresv-benchmarkstagssvcomp14对工具的效果进行评估.

4.1工具实现

本文在现有CPAChecker的基础上，利用谓词抽象、CEGAR、on-the-fly以及时序逻辑等开发了C程序空指针解引用检测工具：NULPChecker.图7给出了该工具的主要框架.CFA模块是基于Eclipse平台的插件，它根据C程序的语法树生成程序的CFA,同时，变量提取模块通过分析CFA提取指针变量.LTL模块根据变量提取模块提取的变量，生成LTL公式，将LTL公式转为与其等价的TGBA，然后和ARG模块进行交互.ARG模块利用on-the-fly的思想，逐步展开CFA和LTL公式,在展开的同时，检查CFA当前状态的命题与公式范式的当前状态是否冲突.重复此过程，直到不再产生新的状态.在没有冲突出现时产生的一条完整路径对应一条反例路径,该路径是否真实存在还需进一步判断.细化模块首先利用SMT求解器判断反例的真实性,如果反例路径是虚假的，则采用插值的方法提取新的谓词,重复上述过程直到给出真反例或证明程序正确.输出模块输出程序的验证结果,验证过程中，可以选择“单个指针”和“所有指针”.

Fig. 7　Core of NULPChecker图7　NULPChecker的中心结构

我们使用NULPChecker检测第3节中的程序中是否存在空指针解引用问题.在检测过程中，工具提示程序中存在一个指针变量，如图8所示，我们选择检测指针变量p是否存在空指针解引用现象.检测结束后，工具提示存在错误路径，如图9所示.

Fig. 8　Choosing pointer.图8　指针选择

4.2实验结果

本文通过NULPChecker检测了程序验证Benchmark程序中的空指针解引用问题，检测结果如表2所示.表2中，列1显示的是测试程序名，列2是程序的行数，列3是程序中指针变量的总数，列4是验证结果安全的指针变量总数，列5是出现空指针解引用问题的指针变量总数.

Table 2　Experimental Data

这里需要指出的是，CPAChecker只支持对加错误标签的位置进行检查，因此，要检查一个指针的所有使用情况，则需要手动地加入很多标签.如果要检测所有的指针，不能保证能够准确地在所有的位置加上合适的标签，而本文的方法无需手动对程序作任何修改.NULPChecker支持对任意C程序中所有空指针解引用的全自动检测，无需人工干预.

5结束语

本文提出了全自动的基于CEGAR的C程序空指针解引用检测方法，并开发了相应的支撑工具.本文的贡献在于指出了程序中常见错误的基于LTL的验证模式.本文针对的是C程序中的空指针解引用问题，但是，所提出的方法也可以用来检测其它问题，如数组越界、除零问题等，这也是本文的后期研究工作.本文给出的模型检测算法目前已经可以对空指针解引用问题进行检测，但是还存在许多缺陷.如果程序存在循环结构，可能会展开多次，最终系统内存不足使程序停止.在分析结构体指针或数组等涉及内存操作的变量时，对变量信息的提取和分析不够完整，会导致程序误报或漏报.程序对C语言的一些复杂的语法结构的支持还不够完善，而且调用的系统函数不能识别其作用，也会导致程序分析结果错误.检查的程序规模虽然有所提高，但是跟待测程序的设计结构有很大关系.有时程序的规模不是很大，但函数之间的调用关系可能会很复杂，如出现递归调用或者循环体的循环次数太大而导致程序堆栈和堆不够用.算法本身会保存很多信息来分析程序，这会占用大量内存.这些问题在后续的研究中都要进行分析.

参考文献

[1]Xiao Qing, Gong Yunzhan, Yang Chaohong, et al. Path sensitive static defect detecting method[J]. Journal of Software, 2010, 21(2): 209-217 (in Chinese)(肖庆, 宫云战, 杨朝红, 等. 一种路径敏感的静态缺陷检测方法[J]. 软件学报, 2010, 21(2): 209-217)

[2]Shapiro M, Horwitz S. Fast and accurate flow-insensitive points-to analysis[C]Pror of the 24th ACM Symp on Principles of Programming Languages. New York: ACM, 1997: 1-14

[3]Ben H, Lin C. Semi-sparse flow-sensitive pointer analysis[J]. SIGPLAN Notices, 2009, 44(1): 226-238

[4]Dalley James L. The art of software testing[C]Proc of National Aerospace and Electronics Conf. Piscataway, NJ: IEEE, 1991: 757-760

[5]Repasi T. Software testing-state of the art and current research challenges[C]Pror of the 5th Int Symp on Applied Computational Intelligence and Informatics. Piscataway, NJ: IEEE, 2009: 47-50

[6]Ellis B J, Ireland A. An integration of program analysis and automated theorem proving[C]Proc of the 4th Int Conf on Integrated Formal Methods. Berlin: Springer, 2004: 67-86

[7]Clarke E M, Grumberg O, Long D E. Model checking and abstraction[J]. ACM Trans on Programming Languages and Systems, 1994, 16(5): 1512-1542

[8]Jhala R, Rupak M. Software model checking[J]. ACM Computing Surveys, 2009, 41(4): 1-21

[9]Beyer D, Henzinger T A, Jhala R, et al. The software model checker Blast: Applications to software engineering[J]. International Journal on Software Tools for Technology Transfer, 2007, 9(56): 505-525

[10]Bayer D, Henzinger T A, Jhala R, et al. Checking memory safety with Blast[C]Pror of the 8th Int Conf on FASE. Berlin: Springer, 2005: 2-18

[11]Condit J, Harren M, McPeak S, et al. CCURED in the real world[C]Proc of SIGPLAN Notices. New York: ACM, 2003: 232-244

[12]Beyer D, Keremoglu M E. CPACHECKER: A tool for configurable software verification[C]Proc of the 23rd Int Conf on Computer Aided Verification. Berlin: Springer, 2011: 184-190

[13]Bayer D, Henzinger T A, Theoduloz G. Configurable software verification: Concretizing the convergence of model checking and program analysis[C]Proc of the 19th Int Conf on Computer Aided Verification. Berlin: Springer, 2007: 504-518

[14]Clarke E M, Kroening D, Lerda F. A tool for checking ANSI-C programs[C]Proc of the 10th Int Conf on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2004: 168-176

[15]Charatonik W, Georgieva L, Maier P. Bounded model checking of pointer programs[C]Proc of the 19th Int Workshop on Computer Science Logic. Berlin: Springer, 2005: 397-412

[16]Frazan A, Madhusudan P, Razavi N, et al. Predicting null-pointer dereferences in concurrent programs[C]Proc of the

20th ACM SIGSOFT Int Symp on the Foundations of Software Engineering. New York: ACM, 2012: 47-57

[17]Dong Yukun, Gong Yunzhan, Jin Dahai. Null pointer dereference defect detecting based on region-based memory model[J]. Acta Electronica Sinica, 2014, 42(9): 1744-1752 (in Chinese)(董玉坤, 宮云战, 金大海. 基于区域内存模型的空指针引用缺陷检测[J]. 电子学报, 2014, 42(9): 1744-1752)

[18]Clarke E. Counterexample-guided abstraction refinement[C]Proc of the 10th Int Symp on Temporal Representation and Reasoning and the 4th Int Conf on Temporal Logic. Piscataway, NJ: IEEE, 2003: 154-169

[19]Tian Cong, Duan Zhenhua. A note on stutter-invariant PLTL[J]. Information Processing Letters, 2009, 109(13): 663-667

[20]Gastin P, Oddoux D. Fast LTL to Büchi automata translation[C]Proc of the 13th Int Conf on Computer Aided Verification. Berlin: Springer, 2012: 53-65

[21]McMillan K L. Lazy abstraction with interpolants[C]Proc of the 18th Int Conf on Computer Aided Verification. Berlin: Springer, 2006: 123-136

[22]Henzinger T A, Jhala R, Majumdar R. Abstractions from proofs[C]Pror of the 31st ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages. New York: ACM, 2004: 232-244

Duan Zhao, born in 1990. Received his MS degree from the Institute of Computing Theory and Technology, Xidian Universiy, Xi’an, in 2015. PhD candidate. His main research interests include software model checking and program analysis.

Tian Cong, born in 1981. Professor and PhD supervisor in the Institute of Computing Theory and Technology, Xidian University. Member of IEEE.Her main research interests include theories in model checking, temporal logics and automata, formal verification of software systems, and software engineering.

Duan Zhenhua, born in 1948. Professor and PhD supervisor in the Institute of Computing Theory and Technology, Xidian University. Senior member of IEEE. His main research interests include model checking, temporal logics, formal verification of software systems, and temporal logic programming.

中图法分类号TP31

基金项目：国家自然科学基金项目(61322202,61420106004,91418201,61133001,61272117)

收稿日期：2015-07-20；修回日期：2015-10-16

This work was supported by the National Natural Science Foundation of China (61322202,61420106004,91418201,61133001,61272117).