可在www.sciencedirect.com在线获取理论计算机科学电子笔记307（2014）33-45www.elsevier.com/locate/entcs非负参数吴雪光1，陈丽倩2，王吉3国防科技大学并行与分布处理国家重点实验室湖南长沙410073摘要程序变量的值域信息在编译器优化和程序分析等许多应用中是有用的。在抽象解释的框架下，区间抽象域为每个程序变量推断出数值界。然而，在诸如自动并行化的某些应用中，通常期望符号范围。在本文中，我们提出了一个新的数值抽象域，即参数范围的抽象域，推断符号范围的非负参数为每个程序变量。这个新的域是基于这样一种认识而设计的，即在某些情况下，程序过程通常具有非负参数，例如输入列表的长度和输入数组的大小。参数范围域试图推断每个程序变量的下限和上限，其中每个界限都是非负参数的线性表达式。参数值域的域运算的时间和内存复杂度为O（nm），其中n是程序变量的个数，m是程序变量的个数是非负参数的个数。在此基础上，我们展示了参数范围的应用，推断符号范围的大小的列表段在程序操作单链表。最后，我们展示了初步的实验结果。关键词：抽象解释，抽象域，区间，符号域。1介绍变量取值的范围信息，即变量取值的上下限，在许多应用中非常有用，包括编译器优化，自动并行化，错误检测等。值范围分析试图在编译时自动推断每个程序变量x的范围[a，b]，这表示约束a≤x≤b。抽象解释理论[8]提供了一个通用框架来计算程序变量的静态近似但合理的值范围。区间抽象域[7]可以发现程序变量值的上下界，但1电子邮件：xueguangwu@sina.cn2电子邮件地址：lqchen@nudt.edu.cn3电子邮件：wj@nudt.edu.cnhttp://dx.doi.org/10.1016/j.entcs.2014.08.0041571-0661/© 2014 Elsevier B. V.保留所有权利。34X. Wu等人/理论计算机科学电子笔记307（2014）33我我发现边界是数值常数。然而，在某些应用中（如自动并行化[3]，符号边界分析[14]和位宽分析[17]），符号范围是需要的。符号范围意味着变量x的边界a和b是除x之外的程序变量的符号表达式。在本文中，我们提出了一个抽象的域，即参数范围，推导符号范围的非负参数为每个程序变量。新的域是基于这样的认识而设计的：在某些应用中，程序过程的参数通常是非负的，例如输入列表的初始长度、输入数组（或存储器区域）的初始大小以及存储器区域的起始地址。参数范围域寻求推断每个程序变量的下限和上限，其中每个界限是线性的。非线性参数的表达式，即，x∈[<$maipi+c，<$mbipi+d]，其中表示程序的第i个非负参数的符号值pr oc ∈ R，ai，bi∈R， c∈R<${−∞}， d∈R<${+∞}. 参数值域的域运算的时间和空间复杂度为O（nm），其中n为整数m是程序变量的个数，m是非负参数的个数。在此基础上，我们展示了参数范围的应用程序来推断符号范围的列表段大小的程序操纵单链表。此外，我们展示了如何结合域的参数范围与一个Quarne等式域推断更复杂的关系。最后，我们展示了初步的实验结果。我们使用图1所示的激励示例来说明用于不变量生成的参数范围的域，该示例具有类型为unsigned int的非负参数n 区间域[7]只能在循环头©处推断x ∈ [0，+∞]。然而，我们的参数范围域推断出x的有趣的符号范围。此外，对于这个例子，由参数范围域生成的不变量与多面体域[9]给出的不变量一样精确public int foo（intn）{unsignedintx;x：=n;如果（x≤2n）为如果（？）则 x：=x+2;elsex：= 2x + 1;©}od}Fig. 1. 一个鼓舞人心的例子本文的其余部分组织如下。第2节讨论了一些相关的工作。第3节给出了参数值域的新抽象域。在第4节中，我们展示了参数范围在列表操作程序中推断列表段大小的符号范围的应用。第5节介绍了我们的原型实现连同初步的实验结果。最后，在第6节中给出了结论以及对未来工作的建议。Loc间隔多面体参数范围©©x∈[0，+∞]x∈[0，+∞]x∈[1，+∞]x∈[n，4n + 2]x∈[n，2n]x∈[n+1， 4n + 2]x∈[n，4n + 2]x∈[n，2n]x∈[n+1， 4n + 2]X. Wu等人/理论计算机科学电子笔记307（2014）33352相关工作值域分析在编译优化、自动并行化和程序分析中受到广泛关注.在抽象解释的框架下，Cousot和Cousot [7]提出了区间抽象域，利用加宽和缩小进行区间分析区间域只能推断变量值的数值界，但由于其线性的时间和空间复杂度，在实际应用中可扩展到大型软件。Blume和Eigenmann [3]提出了在并行化编译器环境中计算符号范围的符号范围传播技术在他们的方法中，变量x的符号范围可以是除了x之外的任意变量的具有max/min算子的非线性表达式。因此，他们的方法在最坏的情况下是指数我们的参数域与他们的不同之处在于：程序变量的参数域是非负参数的线性表达式在我们的方法中，程序变量集和非负参数集是不相交的。这些限制极大地简化了实现参数范围的域运算的算法。由于这些限制，参数范围的域操作的时间和空间复杂度为O（nm）Rugina和Rinard [14]提出了一个用于指针，数组索引和访问内存区域的符号边界分析的框架。它们利用符号多项式表达式来限制用于访问内存的指针和数组索引的范围。他们的方法不是使用固定点算法，而是将符号边界分析问题公式化为符号边界多项式上的约束系统，然后将约束系统简化为线性规划。线性规划的归约步骤是不完全的。此外，线性规划的可靠性要求符号多项式表达式中的所有变量都必须是非负的我们的方法还要求符号范围内的所有参数是非负的。然而，我们的方法只允许线性表达式作为参数范围，并被设计为一个抽象域。我们的分析不需要线性规划。Sankaranarayanan等人[15]提出了一个符号范围约束的抽象域。它们假设程序变量之间的线性排序，并限制变量x的范围，使其包含的变量的阶数严格高于x。我们的域限制了程序变量的范围，使其涉及一组单独的非负参数，而不是其他程序变量。一般来说，我们的域比他们的域表达性差，因为人们总是可以分配比他们域中的程序变量更高阶的非负此外，它们的域允许程序变量之间的显式关系，并且不限制范围内涉及的参数为非负。然而，在时间复杂度方面，我们的域比他们的域便宜我们的参数范围域最接近Venet [16]提出的规范抽象域，该规范抽象域能够有效地推断每个程序变量与循环范围内的所有循环计数器之间的在36X. Wu等人/理论计算机科学电子笔记307（2014）33我我在规范域中，每个程序变量都由一对符号范围近似，这对符号范围是循环计数器上具有整数系数的线性表达式。我们的域的参数范围限制的参数是非负的，但不一定是整数。此外，我们不限制参数范围中的系数为整数。基于规范域的分析将在分析期间为每个级别的循环引入循环计数器，并且因此可以根据循环计数器推断每个程序变量的符号范围。这些循环计数器不能被认为是我们的参数范围域中的参数，因为它们被初始化为零并在分析期间增加。然而，循环边界可以被认为是我们域中的参数，然后我们可以根据循环边界推断程序变量的参数3非负参数3.1域表示让我们考虑一个有n个程序变量x 1，...，xj，.，x n，加上m个非负参数p1，...，pi，.，下午。在实践中，这些参数可以从程序过程的形式参数、只被所考虑的程序过程读取但从不被所考虑的程序过程写入的全局变量、来自I/O设备的输入等中选择我们在抽象域中维护每个程序变量xj的参数范围，表示为xj∈[<$iaipi+c，<$ibipi+d]其中ai，bi∈R， c∈R <${−∞}， d∈R <${+∞}且pi是非线性参数。具体化的定义如下：γ（[iaipi+c，ibipi+d]）={xj∈R|iaipi+c≤xj≤其表示xj的可能值的集合。放松非负性限制。注意，可以放宽参数的非负性限制。如果我们知道参数pi的数值下限c或数值上限d之一，可以取负值或正值，则我们可以引入一个新的辅助非负参数pJi，使得pJd=efpi−c或pJd=efd−pi很容易看出，它总是保持pJi≥0。然后我们可以在整个程序中用pJi+c（或d-pJi）替换所有出现的pi。3.2域操作在我们展示参数范围上的域运算之前，我们首先定义以下非负参数上的线性表达式的序±e（ie），X. Wu等人/理论计算机科学电子笔记307（2014）3337и我 ⎩⎪⎪⎪我⎪⎨我d=efpifibipi+d<$eiaJipi+cjibJipi+d<$eiaipi+c的<$iaipi+c±e<$ibipi+d当且仅当<$p∈[p，p]，<$i（bi−ai）pi+（d−c）≥0（iaipi+ceibipi+difandoifp∈[p，p]，i（bi−ai）pi+（d−c）>0）其中[p，p]表示参数p的数值范围。注意，它总是保持[pi，pi]<$[0，+∞]（其中0≤i≤m）。在我们的实现中，我们首先检查它是否保持，哪里i（bi−ai）pJi+（d−c）≥0（i（bi−ai）pJi+（d−c）>0）如果ai≥bi，则pJ=pipi否则其 中 ch 意 味 着 <$i （ bi−ai ） pi+ （ d-c ） ≥0 （ 或 <$i （ bi−ai ） pi+ （ d-c ） >0 ） 。 然 而 ， 请 注意， i （ bi−ai ） pi+ （ d-c） ≥0d oes 不一定意味着 i（bi−ai）PJi+ （d-c）≥0。我们用φp表示当φi（bi−ai）pi+（d-c）0.现在，我们描述在数值静态分析中使用入选试验。对于同一程序变量x j，两个参数范围之间的包含检验± p定义为[iaipi+c，ibipi+d]±p[iaJipi+cJ，ibJipi+dJ]d=efiajpi+cJ±EMeet. 同 一 程 序 变 量 的 两 个 参 数 范 围 的交集Hpxj定义为[iaipi+c，ibipi+dJ]whee[lexp，lexpJ]否则iai pi+ciflexpd=efiaJipi+cJelseifiaipi+c±eiaJipi+cJiai pi+celseIF⎪⎩ΣiaJipi+cJotherwise38X. Wu等人/理论计算机科学电子笔记307（2014）33⎪⎪⎪⎪⎨我我我我我我我⎪⎨我lexpJd=ef和⎧Σibipi+difΣibipi+d±eΣibJipi+dJlexpJd=efΣibiJpi+dJelseifΣibJipi+dJ±eΣibipi+dibipi+delseIF⎪⎩ΣibJipi+dJotherwise注意，对于lexp，我们试图在iai pi+c和iaJipi+cJ之间选择较小的一个（相对于±e）。当n aipi+c和naJipi+cJ不可比时，我们采用启发式策略，通过比较系数之和，从中选出一个作为新的下界.值得注意的是，根据交集的具体语义，选择iai pi+c或iaJipi+cJ作为结果下界是合理的，即，γ（[iaipi+c，ibipi+d]）<$γ（[iaJipi+cJ，ibJipi+dJ]）H_p [H_ia_j_i_p_i+c_J，H_ib_J_i_p_i+d_J]）.同样的想法也适用于lexpJ的上界。加盟. 为了抽象程序中的控制流连接，我们需要计算同一程序变量xj的两个参数范围的并集。 在本文中，我们计算过近似[lexp，lexpJ]的联合，使两个输入参数范围都包括在[lexp，lexpJ]。连接操作Hp定义如下：[iaipi+c，ibipi+d]Hp[iaJpi+cJ，ibJpi+dJ]d=ef[lexp，lexpJ]哪里lexpd=ef和⎧Σiai pi +cif Σiai pi +c±e ΣiaJipi+cJiaJipi+cJelse ifimin（ai，aJi）pi+min（c，cJ） 或其他如果ibJipi+dJ±eibipi+d，J.P. 我+dJ J.P. 我e + dJelse if 布雷布p我+ d±i=max（bi，bJi）pi+max（d，dJ） o注意，因为对于所有i，我们有pi≥0，它总是成立，（imin（ai，aJi）pi+min（c，cJ））±e（iai pi+c）和（ibipi+d）±e（imax（bi，bJi）pi+max（d，dJ））X. Wu等人/理论计算机科学电子笔记307（2014）3339JJJJp我我？？aJJd=efai≤aJ？ ai：max{l∈T|l≤aJ}J？bJJd=efbi≥bJ？ bi：min{h∈T|h≥bJ}我我我因此，连接操作的结果总是提供两个输入参数范围的过近似。例3.1考虑图1所示的程序。当不动点迭代变得稳定时，在，我们有x∈[n，2n]。在程序点上，应用给定的传递函数，得到x∈[n+2，2n+2]。并在程序点应用else分支的赋值传递函数，得到x∈ [2 n + 1，4 n+ 1]。然后，在控制流连接点©处，我们需要计算连接[n +2，2 n +2] Hp[2 n +1，4 n +1]，这将导致[n +1，4 n +2]。测试传递函数。 任何涉及程序变量（xj）和参数（pi）的条件测试都可以转换为一系列形式为xj≤iaipi+c或xj≥ibipi+d的条件测试，方法是将条件测试约束中的 eachvariablexk（其中ki=j）代入其参数范围。然后我们定义测试传递函数如下：[[xj≤iaipi+c]]#（ρx）d=efρxHp[−∞，iaipi+c][[xj≥ibipi+d]]#（ρx）d=efρxHp[ibipi+d，+∞]其中ρ表示在应用传递函数之前将每个程序变量映射到其符号范围的抽象环境，ρxj表示xj的符号范围。分配传递函数。任何赋值x j：= e，其中e是涉及程序变量（x j）和参数（p i）的表达式，可以通过将e中的每个ch程序变量替换为其参数范围，来转换为形式xj：=[iaipi+c，ibipi+d]的赋值。然后我们定义分配传递函数如下：[[xj：=[iaipi+c，ibipi+d]]]#（ρx）d=ef[iaipi+c，ibipi+d]扩大了的裂缝。有阈值的加宽[2] QT是一个由有限个阈值T组成的加宽参数，包括−∞和+∞。参数范围域的阈值加宽定义为：[iaipi+c，ibipi+d]T[iaJpi+cJ，ibJpi+dJ]d=ef[iaJJpi+cJJ，ibJJpi+dJJ]我我哪里？？cJJd=efc≤cJ？ c：max{l∈T|l≤cJ}我我我⎪djjd=efd≥dJ？ d：min{h∈T|h≥dJ}40X. Wu等人/理论计算机科学电子笔记307（2014）33p⎨⎩⎧p我我pX其中T是一组有限的阈值，包括−∞和+∞。还记得吗：表示条件运算符。直观地说，QT利用具有阈值的区间加宽，参数的每个系数以及常数项。此外，当A还已知程序变量Xj总是非负的，例如，对于类型为unsignedint的情况，xj的参数范围的加宽可以改进为：[iaipi+c，ibipi+d]T[iaJpi+cJ，ibJpi+dJ]d=ef[iaiJJpi+cJJ，ibJiJpi+dJJ]if0±eiaJiJpi+cJ J[0，ibJiJpi+dJJ]，否则其中aJiJ、cJJ、bJiJ、dJJ的定义与上述相同例3.2考虑图2所示的程序，它是从[6]改编而来的。在第一次迭代之后，在©处加宽的输入参数是ρ x：[0。75 n + 1，0. 75 n +1]和ρJx：[0. 6875 n +1，n +1. 25]。 如果我们使用{0，0. 五一一5）与+∞和−∞作为阈值集T，ρ x<$T ρJ将导致[0. 5 n +1，n +1. 5），其中将在随后的递增迭代中保持稳定。public int findDuplicate（int[] nums）{实数x;x：= 0。75例n + 1;while（true）do©if（？）则x：=n+1;否则x：= 0。2500x +0。5n + 1;}od}图二、显示参数范围扩大的示例4表段大小符号范围推断的应用在我们以前的工作[4][5]中，我们已经展示了一种从操纵单链表的程序中导出具有非负整数变量的数值程序的方法其主要思想是：根据指针变量对链表节点的可达性，将一个单链表划分为一组互不重叠的链表段对于每个列表段，我们引入一个辅助的非负整数变量，称为计数器变量，来表示该列表段的大小（即该列表段中包含的列表节点的数量）。在列表操作程序中，经常存在表示输入列表的初始长度的非负参数。因此，在从列表操作程序导出的数值程序中，计数器变量与那些数值变量一起出现在{X. Wu等人/理论计算机科学电子笔记307（2014）3341原始列表操作程序可以被认为是程序变量，而输入列表的初始长度可以被认为是非负参数。在由表操作程序导出的数值程序中，程序变量与参数之间往往存在一种等价关系因此，我们将参数值域的域与一个抽象的等式域结合起来，[12] 进行分析。我们使用参数范围来跟踪每个程序变量的符号范围信息，并使用一个等式来跟踪程序变量和参数之间的一个等式关系。假设有n个程序变量和m个非负参数。然后，该组合域由一个a-rne等式系统Ay=b来描述，其中y= [xp]T，A∈R（n+m）×（n+m），b∈Rn+m，以及程序变量xj∈[xiaipi+c，xiaibipi+d]的符号范围（其中ai，bi∈R，c∈{R，−∞}， d∈{R，+∞}）和非负参数pi∈[CJ，DJ]的数值范围（其中0≤CJ≤DJ）.绑紧了。在组合域中，每个程序变量的符号范围由参数范围域来维护。然而，参数范围可以在一个多项式等式域的域操作期间改变。例如，在一个示例中，当添加了一个A.E.等式时，可以收紧变量的参数范围。 在本文中，我们采用了约束分裂技术， 是一种广泛用于约束编程[1]的约束传播，以收紧参数范围。事实上，组合域的每个一个多项式等式都可以用来收紧其中发生的那些程序变量的参数范围。 Let[xj，xj]表示程序变量x j的参数范围。然后，给定等式iai xi+对于xi，新的候选参数下限来自：xJi=（b−jajpj−jiajxj）/ai其中xj=aj>0 ？xj：xj，和一个新的候选人xi的参数上perbound来自：xJi=（b−jajpj−jiajxJj）/ai其中xJj=aj>0 ？ xj：xj. 如果新的参数范围更小，则xi更新.这个过程可以对等式中的每个变量和系统中的每个等式重复。示例4.1考虑的列表操作程序程序复制并删除（），如图3（a）所示。 它有一个非负参数n作为输入列表x的初始长度。 程序首先将列表x复制到列表p，然后同时删除两个列表。为了证明这个程序的内存安全性，需要一个密钥不变量来证明列表p的长度等于列表x在第11行之后的长度。 此外，如果语句访问下一个字段， 列表变量p（例如，第6，8，13，14行中的语句），我们需要证明p指向的列表段的长度大于或等于1。图3（b）示出了从列表操作程序copy anddelete（）导出的数值程序，其中tpq表示列表变量p和q可以达到的列表段的大小。例如，列表赋值语句图3（a）中的行3上的{y：=x;}意味着在分配之后，x和y指向过去只有x指向的列表段。在赋值之后，很容易看出，将不再有任何列表段，仅由x指向（没有y）。 因此，根据list42X. Wu等人/理论计算机科学电子笔记307（2014）33\→→→→那就} }个文件夹联系我们联系我们void copy and delete（List*x，uintn）void copy and delete num（uintn）1：List*y，p，q; uinttx，ty，txy，tp，tq，tpq;2：假设长度（x）==n;tx：=n;3：y：=x;txy：=tx;tx：= 0;4：q：=p：=null;tp：= 0;tq：= 0;tpq：= 0;5：while（y！null）do while（txy1）do6：y：=y next;tx：=tx+1;txy：=txy-1;7：q：= malloc（）;tp：=tpq;tpq：= 0;tq：= 1;8：q next：=pList;tpq：=tp;tp：= 0;9：p：=q;tpq：=tq+tpq;tq：= 0;10：OD OD11：y：=x;txy：=tx;tx：= 0;12：while（y！null）do while（txy1）do13：y：=y next;tx：=tx+1;txy：=txy-1;14：q：=q next;tp：=tp+1;tpq：=tpq-1;15：free（x）;ty：=txy;txy：= 0;tx：= 0;16：free（p）;tq：=tpq;tpq：= 0;tp：= 0;17：x：=y;txy：=ty;ty：= 0;18：p：=q;tpq：=tq;tq：= 0;19：}od}od} }个文件夹(a)（b）第（1）款图3.第三章。一个列表操作程序（a）及其数字版本（b）。uint表示无符号int。通过赋值，我们可以导出图3（b）中第3行所示的数值语句{txy：=tx;tx：= 0;} 我们建议读者参考[4][5]，了解如何从列表操作程序导出数值程序的在第12行之后，使用参数范围和一个Quarne等式的组合域，我们推断出不变量：{txy−tpq==0，txy∈[1，n]，tpq∈[1，n]， n∈[1，+∞]}。这些创新足以证明第二循环的存储器安全性（即，12号线至19号线5实施和实验我们已经在APRON[11]数值抽象域库中实现了参数范围PA RA的为数值抽象域提供了一个通用接口。我们的实验使用INTERPRO c[13]静态分析仪进行。为了评估PARA的精度和效率，我们比较了PARA与区间域BOX和多面体域NEWPOLKA在APRON中的不变量以及PaRa的性能. 我们的实验是在两组例子上进行的。结果总结于图1A和1B中四比五列“#Vars” gives the number of program variables and “#Pars” gives the numberof 将两个域得到的不变量作为一个整体进行比较“X. Wu等人/理论计算机科学电子笔记307（2014）3343分析输出比右侧分析更强（更弱，等价，不可比）的不变量。当分析仪在2.5GHzPC上运行时，给出了分析时间，该PC具有2G RAM，运行Fedora 12。程序分析结果名称变量数量部分数量BOXInv.PA RAInv.PA RA+AInv.新波尔卡Foo110.006s<0.007s=0.008s=0.012s福韦登110.006s<0.007s=0.008s>0.012s[3]第三季110.004s<0.006s=0.007s=0.011s[第15话]220.005s<0.006s<0.006s=0.012s[第14话]210.006s<0.008s<0.010s=0.016s[10]第10话320.007s<0.010s<0.015s=0.021s[10]第10话220.007s<0.007s<0.010s=0.017s[10]第10话410.008s<0.011s<0.017s=0.021s[16]第12话210.003s<0.004s=0.004s<0.010s[16]第12话200.001s=0.002s<0.004s=0.006s所有上述20120.023s<0.053s<0.092s=/0.335s图四、数值程序的实验结果图4显示了一组小型数值程序的结果。foo和fowiden分别对应于图1和图2所示的程序。带有前缀“e x“的程序上述程序是通过连接图4中列出的所有其他程序来构建的。对于图4中列出的所有程序，除了ex cav12 2（不涉及参数），PA RA给出了比区间域BOX更精确的不变量。与多面体域NEWPOLKA相比，PA RA在大多数情况下生成的不变量精度较低.然而，对于程序fowiden，PA RA生成比New-POLKA更精确的不变量，这是由于PA RA中使用的阈值加宽，其尝试对参数的系数进行阈值。对于除e xipps95和e x cav12 1以外的所有前缀为“e x“的程序 “对于ex cav12 1，图5示出了从列表操作程序手动导出的一组数值程序的结果。这些列表操作程序包含对单链表的常用操作，如创建、遍历、反转、合并、复制、删除和分配。通过连接图5中列出的所有其他程序来构造程序列表。这类由表操作程序派生出来的数值程序往往涉及到程序变量和非负参数之间的一种等价因此，我们利用参数值域和一个不等式的组合域来分析这些程序.在这些程序中， 这些不变量的精度足以证明存储安全性 原始的列表操作程序。44X. Wu等人/理论计算机科学电子笔记307（2014）33程序分析结果名称变量数量部分数量BOXInv.PA RA+AInv.新波尔卡列表创建410.008s<0.011s=0.018s列表遍历310.006s<0.008s=0.016s表反转510.009s<0.015s=0.025s列表长度相等410.007s<0.010s=0.017s列表合并520.009s<0.018s=0.027s列表复制和删除610.007s<0.024s=0.032s表调度710.011s<0.029s=0.040s以上全部列出3480.036s<0.181s=0.826s图五、从列表操作程序派生的数值程序的实验结果6结论我们已经提出了一个抽象的参数范围域来捕获每个程序变量的符号范围，其中每个程序变量的值范围的边界被描述为非负参数上的线性表达式。这个域比区间抽象域更强大。其域运算的时间和空间复杂度为O（nm），其中n为程序变量数，m为非负参数数。作为一个例子来说明新的域的有用性，我们已经展示了它的应用程序来推断分析列表操纵程序的列表段大小的符号范围。它仍然是未来的工作，以考虑在更大的程序和使用参数范围在更多的应用程序，如bufferover bufferow分析的实验。另一个工作方向是考虑使用非负参数的非线性表达式在这种情况下，可以为每个程序变量选择非线性模板。确认我们要感谢匿名评论者的建设性意见。这项工作得到了973计划（批准号：2014CB340703）、国家自然科学基金（批准号：61202120、61120106006、91318301，以及SRFDP，批准号：20124307120034。引用[1] 贝西埃角，约束传播，in：F. Rossi，P. van Beek和T. Walsh，编辑，约束编程手册，Elsevier，2006年。[2] 布朗切特，B.， P. 库索河Cousot，J. 费雷湖 Mau borgne，A. 我的天啊。 Monniaux和X. Ri val，大型安全关键软件的静态分析器，PLDI（2003），pp. 196-207.[3] 布鲁姆，W.和R.Eigenmann，Symbolic range propagation，in：IPPS（1995），pp.357-363.[4] Chen，L.，中国地质大学，R. Li，X. Wu和J. Wang，Static analysis of list-manipulating programs viabit-vectors and numerical abstractions，SAC（2013），pp. 1204-1210。[5] Chen，L.，中国地质大学，R. Li，X. Wu和J. Wang，通过结合形状和数值抽象对列表进行静态分析，计算机编程科学（2014），http://dx.doi.org/10.1016/j.scico.2014.06.004。X. Wu等人/理论计算机科学电子笔记307（2014）3345[6] Chen ， L. ， 中 国 地 质 大 学 ，A.我 没 有 ， J 。Wang 和 P.Cousot ， Anabstractdomaintodiscoverintervallinear qualities，在：VMCAI，LNCS 5944（2010），pp. 112-128[7] Cousot，P. and R. Cousot，Static determination of dynamic properties of programs，Proc.of the 2ndInternational Symposium on Programming（1976），pp. 106-130.[8] Cousot ， P. and R. Cousot ， Abstract Interpretation ： A Unified Lattice Model for Static Analysis ofPrograms by Construction or Approximation of Fixpoints，POPL（1977）。238-252。[9] Cousot，P. and N. Halbwachs，自动发现程序变量之间的线性约束，在：POPL（1978），pp. 84比96[10] Gulwani，S.，Speed：Symbolic Complexity Bound Analysis，in：CAV，LNCS5643（2009），pp. 51比62[11] 让内湾 和A. Mi n′e，Ap ron：Alibraryofnumericalabst ractdomainsforstaticanalysis，in：C AV，LNCS5643（2009），pp. 661-667[12] Karr，M.，程序变量之间的关系，Acta Inf.6（1976），pp. 133-151。[13] Lalire，G.，M.Argoud和B.Jeannet，Interproc，http://pop-art.inrialpes.fr/people/bjeannet/bjeannet-forge/interproc/.[14] 鲁吉纳河和M. C. Rinard，Symbolic bounds analysis of points，array indices，and accessed memoryregions，ACM Trans.程序. 浪系统27（2005），pp.185-235[15] Sankaranarayanan，S.，F. Ivancic和A. Gupta，Program analysis using symbolic ranges，in：SAS，LNCS4634（2007）. 366-383.[16]Venet，A.，规范域：线性不等式不变量的可扩展分析，在：CAV，LNCS7358（2012），pp. 139-154。[17] Zaks，A.，Z.扬岛，智-地Shlyakhter，F. Ivancic，S.卡丹比湾K. Ganai，A. Gupta和P. Ashar，通过符号区间分析减少软件模型检查的位宽，IEEE Trans.集成电路和系统的CAD27（2008），pp。1513-1517年。
我的内容管理
收起
我的收益 登录查看自己的收益
我的积分
登录查看自己的积分
我的C币
登录后查看C币余额
我的收藏 
我的下载 
下载帮助 
