多线程程序数据竞争检测与证据生成方法*

张晓东，郑庆华，刘 烃，俞乐晨，刘 沛，杨子江

( 1.西安交通大学智能网络与网络安全教育部重点实验室，陕西 西安 710049；2.西安理工大学计算机科学与工程学院，陕西 西安 710049)

多线程程序数据竞争检测与证据生成方法*

张晓东1，郑庆华1，刘 烃1，俞乐晨1，刘 沛1，杨子江2

( 1.西安交通大学智能网络与网络安全教育部重点实验室，陕西 西安 710049；2.西安理工大学计算机科学与工程学院，陕西 西安 710049)

数据竞争是多线程程序最为常见的问题之一。由于线程交织导致状态空间爆炸，多线程程序数据竞争引起的错误检测难度大、成本高、精度低；此外，即使检测到数据竞争，由于线程调度难以控制、执行过程难以复现，错误难以复现和定位。提出了一种多线程程序数据竞争检测与证据生成方法，基于程序语义分析和执行过程监测，构建程序的执行路径约束模型和数据竞争条件，将多线程程序数据竞争检测问题转化为约束求解问题，降低检测难度，提高检测精度；利用SMT求解器计算可能的数据竞争，并生成触发该数据竞争的程序执行序列，协助程序员定位和验证错误。实验中对10个程序进行了测试，相比现有数据竞争检测工具threadsanitizer和helgrind，本方法检测出的数据竞争多出287.5%和264.7%，且没有误报，而其他方法平均误报率为10.5%和9.8%。

多线程程序测试；数据竞争；约束求解；证据生成

1 引言

随着处理器多核化的普及，多线程技术已经成为软件编程中提高CPU利用率不可或缺的技术。然而，由于线程之间交织的不确定性，多线程程序执行过程中可能会出现一些难以预料的行为导致程序出错，例如对临界区没有做好同步工作而导致的数据竞争问题。数据竞争是两个不同的线程在没有同步保护的情况下同时访问一个内存，并且至少有一个写操作[1]。数据竞争不一定导致程序错误，因为有些程序员故意让程序有数据竞争以提高运行的效率，但是有调查表明5%～24%的数据竞争会对程序产生坏影响[2, 3]。数据竞争很难被发现，因为它们经常发生在一些低概率出现的交织序列中，在现实中往往需要花很多时间去定位，其引起的错误如同“corner error”，即使在软件发布时也未必能够完全清除它们[4]。因此，数据竞争检测是多线程程序测试领域最受关注的研究点之一。

过去几十年中数据竞争检测已有大量研究，设计出很多杰出的自动化检测工具，主要分为静态[3, 5]与动态分析技术[1, 6～9]。静态方法通过静态检测程序所有的路径来推断程序中的所有数据竞争，可以检测出大部分数据竞争；但由于使用大量假设，静态分析方法会产生无效的数据竞争，导致误报率较高。动态方法通过监控一次执行中内存与同步信息以确定是否存在数据竞争，能够提供较高精度的检测结果。但是，动态分析方法受到交织与路径的影响，往往要通过多次执行来提高覆盖率。本文将静态代码分析与程序执行过程监测相结合，以提高覆盖率且尽可能消除误报。

现有的动态检测技术主要分为三种：基于lockset[1]、基于happens-before[9, 10]与二者结合的方法[6, 11]。(1)基于lockset的方法对线程交织不敏感，但是存在误报情况，即无效竞争。(2)基于happens-before的方法只检测某特定交织序列上的数据竞争，检测结果虽可靠，但敏感于线程交织。(3)混合方法结合了两者的优点，并且试图减少各自的缺点，但也面临如不能够搜索出隐藏的错误、lockset高误报引起的无效报警等问题[4]。

本文提出一种新的多线程程序数据竞争检测方法，根据多线程程序语义构建约束表达式，将数据竞争检测问题转化为可满足性模理论SMT(Satisfiability Modulo Theories)问题，采用SMT求解器求解约束表达式发现可能存在的数据竞争，并生成对应执行路径。本方法主要分为四步：(1)监控程序以得到执行路径；(2)将执行路径转化为无量词一阶逻辑表达式F，此约束表达式涵盖所有可能的线程交织；(3)构建数据竞争候选集合，生成每一个候选发生竞争的条件ρ；(4)遍历候选集合，对每一个ρ求解约束表达式F∧ρ，检查是否存在数据竞争，如果有则生成对应的证据。实验中，设计实现了一个针对Pthread多线程程序的数据竞争检测原型系统，其中采用基于LLVM的插桩工具，其只对内存操作语句以及同步语句进行监控；利用求解器Yices[12]来验证与分析路径信息，以检测出所有数据竞争。另外，本文所提方法能够生成每个数据竞争的证据序列，该序列向程序员展示数据竞争的触发原因。

本文的主要贡献点如下：

(1)提出一种多线程程序约束构建模型，将一次执行中的数据竞争检测问题转化为约束求解问题。此模型按照程序语义进行约束构建，所构建的表达式包含了所有可能的交织序列，进而检测出执行路径中的所有数据竞争。

(2)对所有数据竞争都产生一个证据序列，以给用户提供数据竞争是如何被触发的信息。

(3)对执行序列进行事后分析，不存在on-the-fly技术所产生的巨大运行时开销。

2 动机示例

在此用一个示例来说明本文方法是如何找到路径中的数据竞争。示例程序如图1所示，x与y为共享变量，线程0创建了线程1与线程2。接下来，验证该示例程序是否存在数据竞争的情况。

sharedx,yThread0Thread1Thread21:x=0;4:lock(m);8:lock(m);2:create(1);5:x=a+b;9:x++;3:create(2);6:unlock(m);10:y++;7:y++;11:unlock(m);

Figure 1 Example program

图1 示例程序

随机执行示例程序，生成路径π=[1,2,3,4,5,6,7,8,9,10,11]。对π进行约束构建，所生成的表达式如图2所示。下面逐一解释图2中所有约束的意义与作用。其中，oi表示第i行语句在一次交织序列中的排列序号。

内存模型:o1

Figure2Constraint

图2 约束

内存模型表示程序中变量之间的关系，本文中采用顺序一致性的语义。顺序一致性规定CPU按照代码中语句的顺序来执行程序，所以线程内语句之间的关系如o1

同步约束要求线程之间事件的排序必须按照同步语义，即对线程中lock/unlock操作的约束。在本示例中，要么线程1先获取锁o6

偏序约束要求线程1的首个事件在其创建点之后执行，即o2

竞争条件:数据竞争定义为两个线程同时访问同一内存，且至少有一个写操作。以o6

将图2中所有表达式相与，利用求解器求解，根据结果断定第7行与第10行之间存在数据竞争。同时，根据求解结果对每个事件进行排序，即得到图2中的证据序列。

基于happens-before的方法根据判断事件之间是否存在happens-before关系来断定数据竞争。在路径φ=[1,2,3,4,5,6,7,8,9,10,11]中，由于第7行与第10行之间没有happens-before关系，故检测出二者之间存在数据竞争。但是，如果检测路径φ的其他交织[1,2,3,8,9,10,11,4,5,6,7]，利用happens-before的方法则检测不出数据竞争。这也恰恰说明happens-before方法对线程交织非常敏感的缺点。

虽然基于lockset方法的检测效果不敏感于线程交织，但是检测结果往往会有误报。例如，该方法计算出第1行的锁集为空，第5行的锁集为{m},二者相交为空，即判定此两行之间存在数据竞争，实际上二者不可能并发访问x，检测出的数据竞争是错误的。与基于happens-before的方法相比，本文所提的方法能够检测出执行序列中的数据竞争；与基于lockset的方法相比，能够识别出第1行与第5行不存在数据竞争现象。

3 定义

3.1 事件

本文用事件表示在多线程程序执行过程中观察到的原子执行步。在解决数据竞争问题时，关注的事件类型包括以下两类：共享变量的读与写、线程操作事件(一般有线程创建与终止、锁的获取与释放、条件变量的wait与signal)。事件是计算与分析的基本单位，所以必须要包括足够的信息以助于约束构建。

将事件定义为一个四元组〈tid,type,var,status〉，其中，tid表示线程ID，用于区别事件属于哪一个线程。type表示事件的操作类型，包括读写操作或者线程控制操作。var表示相关变量，如果是赋值语句，则表示共享变量的名字；如果是同步操作语句，则表示互斥量或者条件变量；如果是线程控制语句，则表示为“-”。status表示当type为线程创建或者终止操作时，所控制的线程ID；其他类型的操作都表示为“-”。

例如，事件〈1,read,x,-〉表示线程1对共享变量x进行读操作，事件〈1,fork,-,101〉表示线程1创建线程101。

3.2 路径

在给定输入π下，设定Eπ为多线程程序一次执行中被执行到的事件集合。一条路径τ是指集合Eπ所有事件的一个有序排列，且此排列遵守程序的执行语义。τ与τ的交织序列τ′在线程内的时序关系相同，但线程间的时序关系不同。

3.3 可行序列集合

在同一输入下，每次执行多线程程序都可能会产生不同的交织序列。假设Lπ为偏序集合(E,≼)，其中：

(1)E={e|e∈Eπ}，e表示τ上的事件。

(2)≼表示偏序关系，对于任意em、en∈E：

如果tid(em)=tid(en)且m

如果em为线程创建事件，而en为被创建线程的首个事件，则em

如果em为线程终止事件，而en为被终止线程的末尾事件，则en

≼是传递闭包的。

一条路径一定是一个对Eπ的线性化排列，且遵守顺序一致性的语义。但是，任意一个Eπ的线性化排列即使符合偏序关系也未必是一条执行路径，因为在多线程程序执行过程中事件之间的关系还要受同步语义的约束。

因此，结合Lπ与同步语义约束就构成了所有正确的线性化排列，称之为FLS(Feasible Linearization Set)。验证某一次执行也即是对FLS进行遍历。然而，遍历搜索空间往往非常困难，例如，如果有n个线程，每个线程有k个执行步，则交织数量将达到(nk)!/(k!)n。本文将数据竞争检测问题转化为约束求解问题，借助约束求解器的强大性能来解决遍历难题。

4 数据竞争检测

给定一条多线程执行路径τ，将τ编码为一阶逻辑表达式F，F组成一个包括所有线性排列的搜索空间：

其中，Φpf为路径表达式，Φmo为内存模型顺序约束，Φrw为读写关系约束，Φsyn为同步语义约束，Φpo为偏序约束。从搜索空间中找到所有的数据竞争，并生成每一个触发该数据竞争发生的线性化序列作为数据竞争问题的证据。

4.1 约束构建方法

从线程的角度，也可以定义Eπ={Ti|0

(1)路径表达式(Φpf)。

将每一个线程序列转化为SSA格式，对于每一个SSA格式的执行序列，除去共享访问点都是一个完整的定义-使用链。类似于路径条件(Path Condition)的收集，直接将SSA格式序列转化为路径表达式。此外，本文用符号值来代替系统调用的返回值。

(2)内存模型约束(Φmo)。

在构建内存模型约束时，本文采用顺序一致性模型。顺序一致性语义规定，所有操作完全按程序的顺序执行。那么在此情况下，线程内的事件顺序符合约束：

其中ei与ei+1表示同一线程内连续的两个事件。

(3)读写顺序约束(Φrw)。

路径表达式Φpf定义了线程内定义-使用链，而对于线程间的定义-使用链，则由读写顺序约束Φrw定义。在线程执行时共享变量读取到的值，必须来自最近的写值(包括初始值)。约束Φrw对共享变量的读写关系进行约束，使共享变量的读来自于最近的写。对于同一共享变量，令R作为所有对其进行读操作的事件集合，令W作为所有对其进行写操作的事件集合。给出以下公式：

其中，er为读事件，ew与ex为写事件，vr和vw为事件er与ew所操作的变量。公式的意思是，如果事件er中的vr取值来自于事件ew中的vw，首先要满足er在ew之后，即O(ew)

(4)同步语义约束(Φsyn)。

在多线程程序中表达同步语义的语句主要是lock/unlock与wait/signal操作。互斥变量通过控制线程访问共享数据来实现同步，而条件变量则基于数据的实际值来同步线程。那么，同步语义约束包括这两种操作：

①lock/unlock。

在构建lock同步语义时，在同一互斥锁的lock/unlock集合L中，对于任意两个lock/unlock事件对：li/ui与lk/uk，须满足公式：

在此公式中，锁对li/ui要么发生在锁对lk/uk之前，要么发生在其后。注意，在Φmo中已含有约束O(li)

②wait/signal。

对于条件变量同步语义，要满足条件：每一个wait操作必须对应一个signal操作，而一个signal操作至多唤醒一个wait操作。对于同一条件变量cond，令WT为在cond上所有wait操作的集合，令SG为在cond上所有signal操作的集合。如要满足之上的条件，须有以下公式：

(5)偏序约束(Φpo)。

如果事件创建一个线程，那么被创建线程的所有事件都要在此事件之后执行。如果事件执行join操作，那么被join线程的所有事件都要在此事件之前。本文用偏序关系约束来描述程序中的create/fork/join操作语义。令C为create/fork操作的事件集合，令J为join操作的事件集合。给定约束：

其中，ec为线程创建事件，first(ec)为ec所创建的线程首个事件的顺序；ej为线程终止事件；last(ej)为ej所结束的线程末尾事件的顺序。

(6)数据竞争条件(ρ)。

如果有这样一条路径τ=〈τ1eiejτ2〉，其中τ1是前缀，τ2是后缀，事件ei与ej属于不同的线程并且都访问同一内存，至少有一个写，那么二者之间发生了数据竞争，而看作是与数据竞争的证据序列。

4.2 数据竞争检测方法与证据生成

给定候选数据竞争发生的条件ρ，验证是否存在一条交织序列使得ρ成立。因为搜索空间F包含了在给定输入下所有可能的线程交织序列，所以将搜索空间F与数据竞争条件ρ合并，生成程序数据竞争表达式：

利用SMT求解器来检查公式Fveri的可满足性，判断程序是否可能发生数据竞争。如果无解，说明此候选数据竞争不会发生；如果有解，说明存在数据竞争。在有解的情况下，生成一条触发该数据竞争的证据序列提供给用户，此序列与操作系统与运行时环境无关，可以指导程序员定位和修改错误。由此，数据竞争的检测问题即转化为SMT求解问题，大大减轻了交织组合爆炸问题。

数据竞争的验证过程如算法1中所示，通过遍历DRCS来验证所有数据竞争。如果Result为sat，则说明此候选满足竞争条件，同时根据求解结果计算出触发序列，此触发序列即是证据；否则，继续遍历DRCS。在遍历的过程中，对每一次F∧ρ，利用SMT求解器的增量求解机制来减少求解的开销[12]。

算法1验证框架

输入：所有候选数据竞争的发生条件(DRCS)与搜索空间F;

输出：所有数据竞争以及对应的证据序列。

For eachρ∈DRCS

Result= SMT_Solving(F∧ρ);

If (Result== sat) Then

Report this data race and output its witness;

Else

Continue;

4.3 计算复杂度

假设事件数量为n，全局访问点为m，同步操作语句lock/unlock数量为l，fork与create语句数量为k，则内存模型约束的复杂度为O(n)，同步语义约束的复杂度为O(l(l-1))，偏序约束的复杂度为O(k)，候选数据竞争约束的复杂度为O(m(m-1))。因此，本方法构建的约束表达式复杂度为多项式O(n+l(l-1)+m(m-1))，其约束构建与求解的开销都在可接受范围之内。

5 验证测试

在LLVM[13]平台上实现了多线程程序约束构建，在LLVM中间字节码的粒度上，通过插桩程序并监控程序运行过程、记录执行路径。然后，根据4.1节中设计的约束模型，析取该执行路径下程序的各类约束表达式。利用Yices[12]作为SMT求解器，检测是否存在数据竞争。实验是在ubuntu 12.04环境下进行的，处理器是i5 3.2 GHz，内存是4 GB。与现有数据竞争检测工具tsan[8]与helgrind[9]进行了对比(tsan结合happens-before与lockset方法，helgrind是基于happens-before的方法)。

在测试程序中，example是C语言实现的示例程序；程序carter、stateful、account、twostage选自文献[14]；dekker、lamport、peterson、szymanski与time_var_mutex这五个程序来自于文献[15]。对所有的测试程序，利用tsan、helgrind与本文方法进行分析比较，实验结果如表1所示。在表1中，列LoC表示源码行数，#T表示线程数，#SAP表示共享访问点，Time表示计算开销，其中包括判断是否有数据竞争以及生成反例，最后一行Avg.表示各项指标的平均值。从实验数据中得知，当共享访问点较多时，分析时间相对较长。本文方法属于事后分析，在时间方面不与threadsanitizer与helgrind进行比较，将重点对比在数据竞争检测数量(N)与误报率(FP)上的差别。

对于carter、stateful、account、twostage，本文方法检测出的竞争数量与threadsanitizer、helgrind相同，且误报率都为零。

在检测example、dekker、lamport、peterson、szymanski与time_var_mutex时，本文方法所检测出数据竞争的数量超过其他两者。尤其是szymanski，本文方法可以检测出34个有效数据竞争，多于其他两者。

对于dekker、lamport、peterson、szymanski，此四程序并不是由锁,而是由循环语句来控制同步的。

其他两者在处理类似图3中所示的情况时，o1与o3会被认为是数据竞争。但是，根据值传递与语义的限制(o1要执行在o2之前)，o1与o3不可能并发执行。例如，在检测dekker所产生的四个数据竞争中[15]，其他两者会误报第22行x=0与第39行x=1存在数据竞争，但其实两者中间有第23行assert(x≤0)，限定执行中第22行要在第23行之前，而第39行必须在第23行之后。本文方法则利用路径表达式与读写关系约束限制程序按照正确语义执行，不会误报此类无效数据竞争。

AB……1:x=02:while(x==0);…3:x=1…

Figure 3 Spurious race

图3 假竞争

经过实验数据比对，tsan与helgrind在检测此四程序时误报率较高，其中tsan平均为29%，helgrind为27%。相比，本方法在误报率方面低于工具threadsanitizer与helgrind。

6 相关工作

在数据竞争检测方面已经有很多方法。其中可以分为动态、静态、动静结合。静态分析工具是通过对源代码进行分析以输出代码中的所有数据竞争，当然存在一定的误报问题[3, 16]。动态检测方法是通过将运行时分析类库注入到被测程序中，在具体运行程序时进行数据竞争的预测，这种方法虽然只能检测出执行路径上的数据竞争，但是误报较少[1, 8, 9]。动静结合的方法是先静态找出所有可能的数据竞争，然后只监控可能发生数据竞争的内存，最后再利用动态分析方法检测程序[4]。

Table 1 Experimental results表1 实验结果

实际上，动态分析方法所带来的运行时开销是很大的，相关研究人员已做了很多工作以减少运行时开销。Marino D等人[10]设计了工具LiteRace，通过抽样监控内存来减少运行时开销。Kasikci B等人[4]通过减小监控范围在一定程度上减小了运行时开销。还有一种方法通过加大监控内存的粒度来降低运行时开销，但是同时也有误报[17]。

Wang C等人[18, 19]利用执行路径与程序源码构建一个符号化的预测模型，以检测并行程序中断言预测与原子性违背问题。本文方法的思想一部分来自于Said M等人在文献[20]中提出的方法，用于实现数据竞争的预测以及路径的还原。但是，文献[20]中只处理了Java程序路径中某一个数据竞争，而本文是针对路径中所有的数据竞争。

7 结束语

本文提出了一种多线程程序数据竞争检测与证据生成方法，通过对一条执行路径进行约束建模，将数据竞争检测问题转化为约束求解问题，利用现有约束求解器分析出一条执行路径中所有可能的数据竞争，并且对于每个数据竞争都给出触发证据序列。本方法将数据竞争静态检测与动态监测相结合，有效降低分析的复杂度和检测的误报率。本研究通过构建多线程程序的约束模型，将程序测试转化为约束求解的方法，可以避免由于多线程程序线程交织导致的状态空间爆炸问题，该思路为软件覆盖性测试，特别是多线程程序测试提出了新的解决方案。

[1] Savage S, Burrows M, Nelson G, et al. Eraser:A dynamic data race detector for multithreaded programs[J]. ACM Transactions on Computer Systems (TOCS),1997, 15(4):391-411.

[2] Erickson J, Musuvathi M, Burckhardt S, et al. Effective data-race detection for the Kernel[C]∥Proc of OSDI’10, 2010:1-16.

[3] Voung J W, Jhala R, Lerner S. RELAY:Static race detection on millions of lines of code[C]∥Proc of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2007:205-214.

[4] Kasikci B, Zamfir C, Candea G. RaceMob:Crowd sourced data race detection[C]∥Proc of SOSP’13, 2013:406-422.

[5] Wang L, Stoller S D. Runtime analysis of atomicity for multithreaded programs[J]. IEEE Transactions on Software Engineering, 2006, 32(2):93-110.

[6] Xie X, Xue J, Zhang J. Acculock:Accurate and efficient detection of data races[J]. Software:Practice and Experience, 2013,43(5):543-576.

[7] Wester B, Devecsery D, Chen P M, et al. Parallelizing data race detection[C]∥Proc of ASPLOS’13, 2013:27-38.

[8] Serebryany K, Iskhodzhanov T. ThreadSanitizer:Data race detection in practice[C]∥Proc of WBIA’09, 2009:62-71.

[9] Helgrind:A data race detector[EB/OL].[2007-01-01].http://valgrind.org//docs/manual/hg-manual.html.

[10] Marino D, Musuvathi M, Narayanasamy S. LiteRace:Effective sampling for lightweight data-race detection[C]∥Proc of PLDI’09, 2009:134-143.

[11] Flanagan C, Freund S N. FastTrack:Efficient and precise dynamic race detection[C]∥Proc of PLDI’09, 2009:121-133.

[12] Dutertre B, De Moura L. A fast linear-arithmetic solver for DPLL(T)[M]∥Computer Aided Verification, Berlin Heidelberg: Springer,2006:81-94.

[13] Lattner C, Adve V. LLVM:A compilation framework for lifelong program analysis & transformation[C]∥Proc of TACAS’08, 2008:75-86.

[14] Cordeiro L,Fischer B.Verifying multi-threaded software using SMT-based context-bounded model checking[C]∥Proc of ICSE’11, 2011:331-340.

[15] Gupta A,Popeea C,Rybalchenko A.Threader:A constraint-based verifier for multi-threaded programs[M]∥Computer Aided Verification, Berlin Heidelberg:Springer, 2011:412-417.

[16] Engler D,Ashcraft K.RacerX:Effective,static detection of race conditions and deadlocks[C]∥Proc of SOSP’03, 2003:237-252.

[17] Von Praun C, Gross T R. Object race detection[C]∥Proc of OOPSLA’01, 2001:70-82.

[18] Wang C, Limaye R, Ganai M, et al. Trace-based symbolic analysis for atomicity violations[M]∥Tools and Algorithms for the Construction and Analysis of Systems, Berlin:Springer, 2010:328-342.

[19] Wang C, Kundu S, Limaye R, et al. Symbolic predictive analysis for concurrent programs[J]. Formal Aspects of Computing,2011,23(6):781-805.

[20] Said M, Wang C, Yang Z, et al. Generating data race witnesses by an SMT-based analysis[C]∥Proc of NASA Formal Methods, 2011:313-327.

ZHANGXiao-dong,born in 1990,PhD candidate,CCF member(E200034811G)，his research interest includes program analysis.

Adataracedetectionandwitnessgenerationmethodformultithreadedprograms

ZHANG Xiao-dong1，ZHENG Qing-hua1，LIU Ting1，YU Le-chen1，LIU Pei1，YANG Zi-jiang2

(1.MOE Key Laboratory for Intelligent Networks and Network Security,Xi’an Jiaotong University,Xi’an 710049;2.School of Computer Science and Engineering,Xi’an University of Technology,Xi’an 710049,China)

Data race is a common problem in multithreaded programs. Due to the state explosion of thread interleaving, it is difficult to accurately detect bugs triggered by data races. Moreover, it is hard to replay and triage such bugs because of the facts that thread scheduling is difficult to control and the number of interleaving is astronomically large. A data race detection and witness generation method for multithreaded programs is proposed. A semantic model is designed to encode the execution path and the condition of data races as first-order logic formula. The satisfiability of the formula, solvable by constraint solvers, indicates the existence of data races under multiple thread interleavings without requiring repeated executions. The solutions produced by an SMT solver serve as witnesses to localize and verify data races. In the experiments, we compare existing tools threadsanitizer and helgrind with ours to detect the data races for 10 multithreaded programs. It is shown that our method can detect 287.5% and 264.7% more bugs respectively without false alarm, while the false alarm positive rate of threadsanitizer and helgrind are 10.5% and 9.8%.

multithreaded program testing;data race;constraint solving;witness generation

1007-130X(2014)11-2047-0

2014-06-06;

：2014-08-31

国家自然科学基金资助项目(91118005,91218301,61221063,61203174)；国家863计划资助项目(2012AA011003)；国家科技支撑计划(2012BAH16F02)；教育部创新团队资助项目(IRT13035)；中央高校基本科研业务费专项资金资助项目

TP311

：A

10.3969/j.issn.1007-130X.2014.11.001

张晓东(1990),男,河南民权人，博士生，CCF会员(E200034811G)，研究方向为程序分析。E-mail:xdzhang@sei.xjtu.edu.cn

通信地址：710049 陕西省西安市西安交通大学智能网络与网络安全教育部重点实验室

Address:MOE Key Laboratory for Intelligent Networks and Network Security,Xi’an Jiaotong University,Xi’an 710049,Shaanxi,P.R.China