多面体数值域在程序变量关系检测中的实用性与精度分析 - 马尔科·鲁比诺 Università di Chieti-Pescara

≤≤·≤≤可在www.sciencedirect.com在线获取理论计算机科学电子笔记334（2018）3-16www.elsevier.com/locate/entcs数值域推断距离马尔科·鲁比诺Università di Chieti-Pescara，佩斯卡拉，意大利摘要在用于检测程序变量之间的线性关系的数值抽象域中，从纯理论的角度来看，多面体域是最精确的一个。其他领域，如间隔，八边形和平行体，表达能力较低，但通常更有效。我们把注意力集中在区间约束，并使用一套基准，我们的实验表明，在实践中，多面体可能会经常计算结果不太精确比其他域，由于使用的加宽算子。关键词：静态分析，抽象解释，数值域，多面体，加宽。1介绍许多数值抽象域已经在文献中定义，目的是发现命令式程序中数值变量之间的关系。这些抽象域在可以表示的程序变量上的约束的形状和数量上不同最常见的数值域是区间[14]、八边形[20]和多面体[15]抽象域。区间的定义域Int对形式为x的约束的有限集合进行编码u或lx，其中x是程序的变量，l，u分别是表示下限和上限的数字。这是非关系域的一个经典例子，因为它不能显式地表示两个不同程序变量之间的关系。相反，多面体的域Poly能够表示程序变量上的任何有限的线性约束集。每个线性约束具有a xu的形式，而它们中的有限个可以表示为Ax u，其中A是系数矩阵，x是程序变量的向量，u是程序变量的向量。1 电子邮件：{gianluca. unich.it，marco. unich.it}https://doi.org/10.1016/j.entcs.2018.03.0021571-0661/© 2018作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。4G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）3≤≤≤{−}·≤≤→上界Poly是一个关系域，因为每个约束可能涉及许多不同的变量。最后，八边形的域Oct位于其他两个之间：它可以表示最多两个程序变量的约束，但仅具有ax+by u的形式，其中a，b为1，0，1。这些被称为八边形约束。Oct是所谓的弱关系域的一个典型例子。这类域允许表示涉及不同变量的约束，但约束的形式受到严格限制。interval和octagon抽象域也是模板抽象域的例子[22]。这是可以表示任何线性约束a xu的所有域的族，但是可用系数向量a的集合是先验选择的，并且在分析期间不能改变。每个抽象对象可以表示为AX u，其中A是模板矩阵，u是上界向量。 它可能看起来与多面体相同，但根本的区别在于，在多面体抽象域中，系数矩阵A可以在分析期间自由变化，而在模板抽象域中，模板矩阵A是固定的。例如，对于区间域，A是矩阵（I| −I）T.这些域的广泛使用至少部分是由于它们在两个最着名的数值抽象域库中实现，即APRON[18]和PPL[12]。在文献中有许多其他的模板抽象域，也有不属于这一类的域的例子，尽管它们不如多面体精确。例如，TVPI [23]（每个线性不等式两个变量）可以表示ax + by u形式的有限约束集，而对a和b没有任何限制。这是一个弱关系抽象域，因为它只能编码两个变量之间的关系，而不能编码模板域。另一例子是parallelotopes的域Par[8]，在Jandom静态分析器中实现[3]。 这个域中的抽象对象可以表示为Ax u，如多面体域，但要求系数矩阵A是可逆的。因此，如果与多面体相比，平行六面体的表达能力有限，尽管它们不属于模板或弱关系域的类别。 存在平行体结构域的模板变体[4，5]，但 在本文中不使用它抽象域本文的目的是从分析可达到的精度的观点出发，对一系列抽象域，包括区间、八边形、多面体和平行六面体，进行实验比较。在理论水平上比较抽象领域的精确性是困难的，因为一个领域的更强的表达能力并不总是产生更精确的整体分析。一个数值抽象域被形式化为一个由≤A预排序的抽象属性的集合A，并被赋予单调性（w.r.t.具体化映射γ：A <$（Rn）中的子集序，其中n是程序变量的个数.我们说域A比域B更有表现力，我们写A> B，如果G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）35γA是γB的象的严格超集。根据表现力，我们有Poly>Oct>Int和Poly>Par>Int，而八边形和平行四边形是无法比拟的。显然，域越有表现力，它就越能准确地跟踪程序执行期间程序变量的值，至少在原则上是这样。如果我们比较使用域A和B进行的两个分析，其中A > B，我们会期望使用A的分析比使用B的分析找到更多的约束或更精确的边界。然而，领域的表现力并不能说明全部。至少有另外两个因素可能会影响分析结果：抽象运算符和扩展。如果抽象算子不是具体算子的最佳正确近似，则分析的结果可能不会尽可能精确。虽然用于区间、多面体和八边形的抽象运算符通常被实现为具体运算符的最佳正确抽象，但这不会发生在paral- lelotopes上。原因是对于平行体上的许多运算符来说，没有最好的正确抽象。这是因为，给定Rn的一个子集，一般不存在最小平行体逼近它，而是存在许多最小竞争平行体，启发式考虑用于在不同的最小位置中进行选择请注意，同样的情况也发生在多面体上（例如，球体没有最佳多面体近似），但这对于静态分析来说不是一个大问题，因为在这种情况下使用的大多数操作都将多面体转换为多面体（因此，Poly中的抽象运算符大多是γ-完备的[7]）。然而，对分析精度的更大影响可以说是通过扩大。对于模板域，加宽的实现是简单的：由于约束的数量和形式是固定和有限的，我们只需要将边界扩大到无穷大以强制终止分析。然而，对于非模板域，约束可以在每次迭代中自由地改变。因此，加宽操作者有更多的自由度，可以尝试不同的解决方案来确定一组稳定的约束。对于多面体域，使用中最常见的加宽是[15]中描述的所谓标准加宽，后来在[17]中进行了改进，以及[11]中描述在下文中，它们将被称为H79和BHRZ03加宽，采用PPL中使用的名称。加宽H79在当前迭代的多面体中的所有点满足约束的条件下，保持先前迭代中多面体的所有约束。加宽BHRZ03通过结合四种不同的启发式技术，从上限运算符得到改进的标准加宽这两种加宽都存在这样的情况，即它们以这样的方式失去精度，使得所得到的分析不如即使用简单得多的区间域所能达到的精确。详细的例子见[21]。平行六面体上的加宽不同于多面体上的加宽，因为它根据在两个连续迭代中评估平行六面体之间的距离的启发式，动态地选择用于结果的整个系数矩阵，或者是先前迭代的系数矩阵，或者是新迭代的6G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）3抽象域从理论的观点来看，研究抽象算子在空间和时间上的计算复杂性是很容易的。区间上的大多数运算在变量数上是线性的。对于八边形和平行六面体，运算在变量数量上至多是立方的，而多面体在变量数量上具有最坏情况下的指数复杂度。然而，仅仅知道每个抽象运算符的行为并不能完全说明域在实际分析中的性能。特别地，预测多面体的行为是困难的，因为操作的成本很大程度上取决于在分析期间发现的多面体的复杂性。因此，存在多面体比八边形快的情况，以及多面体比八边形快的情况。 要慢得多。另一个可能影响性能的因素是分析的收敛速度。从这个角度来看，任何试图通过减少加宽和缩窄的效应来提高精度的尝试（例如，延迟加宽或带阈值的加宽[13]）通常会增加分析所需的时间相对精度在本文中，我们将重点比较的精度分析运行相同的算法，但不同的域。然而，我们不直接比较分析返回的结果，原因有二。首先，我们会得到许多不可比的结果。第二，域，如平行六面体和多面体，发现许多复杂的约束，涉及大量的变量，虽然可能是有用的跟踪程序的执行，并不是特别有用的最终结果。一般来说，更简单的约束更容易应用。例如，间隔约束可以用来证明一些运行时错误，如被零除或对数组的越界访问，在实践中不会发生。在需要的情况下，简单的程序变换可以用新的合成变量替换复杂的表达式此外，区间约束是最大的一组约束，可以显式地表示在所有的域。基于这些原因，我们认为仅在区间约束上评估分析的精度是一种有价值的方法。为了完整性，我们还对八边形约束进行了不同的比较。这些约束非常有用，例如，当数组创建时，其维度仅在运行时已知，则可以检查是否存在越界数组访问。然而，由于可能会创建新的合成变量，将所有问题转换为区间检查问题，我们认为这种比较不像区间约束那样相关。G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）37−−∞2实验评价我们已经进行了实验评估，以比较不同的数值抽象域的相对精度间隔的限制。我们考虑了以下域：区间、八边形、多面体、平行面以及平行面与区间的约化积。对于平行空间，有几个变体是可用的，这些变体在用于抽象操作的抽象中是不同的，这些抽象操作没有最佳正确的抽象。特别地，我们使用了变体Par+axes[6]，其中抽象操作更倾向于生成其约束矩阵包含区间约束的平行体。相反，在平行体和区间的约化积中，我们使用了变量Par−axes，其中抽象运算生成几乎不使用区间约束的平行体。对于多面体，由于我们对加宽对实际精度的影响感兴趣，因此我们考虑两种变体，一种使用H79加宽，另一种使用BHRZ 03。使用Jandom静态分析器[3]在ALICe基准测试[19]上进行基准测试Jandom是一个简单命令式程序、线性转换系统和Java字节码的分析器Intervals、parallelotopes及其乘积在Jandom中原生实现。对于八边形和多面体，我们使用PPL中的实现。测试套件包括总共108个模型（线性过渡系统），总共326个位置，其中161个是回路头。每个模型最多有11个不同的位置，4个循环头和10个变量。大多数模型（108个中的102个）是ALICe基准测试的一部分，其余6个来自我们以前的工作。对于每个模型进行经典的两阶段分析，包括一个上升链与扩大和下降链与缩小。加宽和变窄应用于所有环头。对于多面体，使用总是返回下降链的前一个值的平凡收缩。延迟应用于加宽和缩小。我们已经试验了不同的延迟值：对于加宽，我们使用0到6之间的值，而对于缩小0到3之间的值。这里没有示出以更大的窄化延迟进行的进一步实验，因为实际上没有改进。所有结果均可通过在Jandom的nsad17分支，在GitHub2上可用。2.1时滞加宽和缩窄对区间约束的影响表1示出了对于每个域和每个延迟设置，通过分析发现的非平凡区间约束的数量。 给定一个抽象对象S和一个程序变量x，我们确定S中线性形式x的最大值。 如果它是一个实数或（这是可能的，当S是空的），我们已经找到了一个非平凡的区间约束。同样的情况也适用于线性形式x。表中出现的值是通过对非平凡的2https://github.com/jandom-devel/Jandom8G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）3H增宽延迟缩小延迟域01234560间隔889890907919919920923八角形878878880899922920920无柄类847848876883884884884Par−axesH Int905921935946962961980多面体H79783771729752778794800多面体BHRZ037797857918078268388461间隔889890907919919920923八角形878878880899922920920无柄类850851881886886887887Par−axesH Int912926940953963966983多面体H79921909863879885889893多面体BHRZ039019079099129219239272间隔889890907919919920923八角形878878880899922920920无柄类850851881886886887887Par−axesH Int914928939955965968985多面体H79930918870886888892896多面体BHRZ039099129149209259279313间隔889890907919919920923八角形878878880899922920920无柄类850851881889889890890Par−axesH Int910925942952962965982多面体H79930918870886888892896多面体BHRZ03909912914920925927931表1通过分析发现的非平凡区间约束的数量为每个模型的每个位置找到间隔约束缩小延迟为0的情况对多面体非常不利，因为这意味着根本不执行下降链。它只是为了完整性而显示，但在实践中并不特别有趣。实际上，如果我们排除多面体域，延迟缩小似乎有一个非常边际的好处。特别是对于间隔和八边形，结果没有显示延迟狭窄的任何改善。事实上，下降链一般都很短，已经观察到[1，2]。延迟加宽的情况非常不同。在这种情况下，所有的域，除了多面体与H79加宽，逐渐提高精度时，延迟增加。这个规则有一些小的例外，比如当延迟从4增加到5时，八边形会失去精度，当缩小延迟为0而扩大延迟从4增加到5时，Par−axesInt最后，具有H79加宽的多面体很难与延迟加宽相结合：从延迟0到延迟2，精度会丢失。 从延迟3开始，分析恢复了一些丢失的精度，但它永远不会恢复到延迟0时的精度。G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）39- -2.2比较域名w.r.t.区间约束通过比较不同区域的结果，我们可以看到，从加宽延迟2开始，平行体和区间的约化积是能够找到最多非平凡区间约束的区域。当不使用延迟加宽时，具有标准加宽的多面体是最好的，而具有高延迟的多面体是最差的它的结果在任何情况下都小于具有Par−axesHInt的最佳结果显然，对于给定的变量，位置和模型，两个域可以找到具有不同边界的非平凡区间约束在表2中，我们展示了一些这些结果试图考虑到这一事实。在此表中，对于每个加宽和缩小延迟以及每个域，我们显示了由域发现的非平凡区间约束的数量，其边界不比由其他域推断的边界差我们仅显示延迟狭窄1和2的结果，这是最重要的病例。 虽然数字略有不同，但它们在结果与表1所示一致。增宽延迟缩小延迟域01234561间隔856857873877877878881八角形854854856871893891890无柄类825826856855855856856Par−axesH Int893908922930940942955多面体H79917905858874877881885多面体BHRZ039019079099129219229252间隔856857873877877878881八角形853853855870892890890无柄类825826856854854855855Par−axesH Int891904917930940942953多面体H79924909863879878882886多面体BHRZ03909912914920925927931表2通过分析发现的具有最佳界w.r.t.的非平凡区间约束的数量。其他域缩窄延迟1或2的结果非常相似。图1以图形方式显示了表2第一行中包含的值，其中缩小延迟设置为1。可以立即看到，多面体BHRZ03发现的更好的区间约束边界的数量在增加加宽延迟时严格增加。对于多面体H79，情况并非如此，多面体H79仅在小的加宽延迟方面优于其他域。在表4中，我们从不同的角度显示了相同的数据。对于每个选择的加宽和缩小延迟以及每个域，表中包含一对+m/ n。这里，+m（n）意味着给定的域已经找到了，对于m（n）个区间约束，一个比多面体BHRZ 03找到的严格更好（更差）的边界。实验表明，所有域（多面体除外具有加宽延迟至少2）的H79能够找到至少一个间隔约束10G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）3HH一千9809609409209008808608408200 1 2 3 4 5 6增宽延迟Fig. 1. 表2比多面体BHRZ 03有更好的边界，换句话说，我们几乎在所有情况下都有m >0另一方面，比较正数和负数，我们可以看到，在大多数情况下，n几乎是m的两倍。唯一的例外是域Par−axesInt，其中当加宽延迟不为0时，m > n特别地，增加加宽延迟，具有更好界限的区间约束的数量增加，直到m几乎是n的两倍。这种比较表明，平行表，虽然它可能不是一个很好的域时，单独使用，是能够提高精度的其他抽象域时，在减少产品。2.3八角形约束表3与表2的八边形约束类似。我们省略了表1的类似内容，因为我们认为它不相关：所有域都找到了许多非平凡的次优八边形约束，就像两个区间约束的组合一样。我们看到多面体给出了比Oct本身更精确的边界（除了缩小延迟0，如前所述，这对多面体不公平）。Intervals和parallelotopes给出了最差的结果，而octagons和Par−axesInt是可比较的。然而，我们认为平行六面体和八边形的一个假设的简化积将占据首位。结果间隔八角形表 位H级内部P−H79轴多面体多面体BHRZ03G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）311增宽延迟缩小延迟域01234560间隔1897190019441971196019631981八角形2533251325222602267826762670无柄类1988199120772089208120812080Par−axesH Int2448249424992500255325232556多面体H792507247123032420247625302598多面体BHRZ0324532482250525812648271427811间隔1888189219361954195219551973八角形2520250225092584266526612658无柄类1992199620902091208920922091Par−axesH Int2455249725462555262125952622多面体H792948290527082778273827552821多面体BHRZ0328612880288829152919295730082间隔1888189219361953195219551973八角形2516249825052580266126572656无柄类1988199220902087208620892088Par−axesH Int2445248425272548262225912600多面体H792969292327202788274127582824多面体BHRZ0328822896290429342927296830213间隔1888189219361953195219551973八角形2516249825052577265826542653无柄类1992199620902093209220952094Par−axesH Int2431247725332515261025832614多面体H792969292327202788274127582824多面体BHRZ032882289629042934292729683021表3通过分析发现的具有最佳边界w.r.t.的非平凡八边形约束的数量。其他领域。增宽延迟缩小延迟域01234561间隔+56/-101+54/-104+65/-101+64/-99+55/-99+55/-99+54/-99八角形+56/-103+53/-106+53/-106+59/-100+65/-93+62/-93+58/-93无柄类+53/-129+51/-132+62/-115+63/-120+56/-122+56/-122+52/-122Par−axesH Int+58/-56+58/-47+65/-43+72/-44+74/-45+69/-39+72/-32多面体H79+33/-17+19/-21+0/-51+0/-38+0/-44+0/-42+0/-42多面体BHRZ03+0/-0+0/-0+0/-0+0/-0+0/-0+0/-0+0/-02间隔+51/-104+49/-104+60/-101+59/-102+54/-102+53/-102+52/-102八角形+51/-107+48/-107+48/-107+51/-101+61/-94+57/-94+53/-94无柄类+49/-133+47/-133+58/-116+59/-125+55/-126+54/-126+50/-126Par−axesH Int+53/-61+54/-52+60/-48+66/-46+72/-47+66/-41+68/-34多面体H79+32/-17+18/-21+0/-51+0/-41+0/-47+0/-45+0/-45多面体BHRZ03+0/-0+0/-0+0/-0+0/-0+0/-0+0/-0+0/-0表4区间约束的数量，对于该区间约束，域改进/降低了关于BHRZ03加宽的多面体12G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）3增宽延迟缩小延迟域01234560间隔37± 833± 339± 742± 451± 553± 557± 4八角形624± 269477± 57741± 340551± 44810± 439657± 55698± 71无柄类1426± 271594± 261685± 171966± 162228± 952420± 292781± 22Par−axesH Int3915± 274251± 524776± 385194± 545077± 246133± 277035± 52多面体H79591± 106669± 150768± 136753± 37907± 98974± 991214± 42多面体BHRZ03803± 1611004± 605737± 881011± 3271097± 821356± 1312357± 2911间隔33± 534± 340± 548± 949± 348± 363± 9八角形528± 104553± 34539± 70738± 283619± 23730± 264777± 95无柄类1435± 301605± 241716± 201982± 102268± 222592± 1442884± 19Par−axesH Int4133± 304468± 635029± 105407± 435488± 436522± 487311± 55多面体H79719± 85642± 25812± 95880± 136947± 1061155± 1901258± 65多面体BHRZ03804± 113867± 124978± 1381007± 911115± 1361384± 1082362± 972间隔31± 438± 577± 8844± 651± 9109± 11955± 5八角形484± 74537± 41633± 233582± 46609± 34786± 285825± 289无柄类1428± 141604± 291717± 232028± 952325± 1252550± 482889± 40Par−axesH Int4400± 74741± 305300± 135719± 1375777± 356662± 267613± 18多面体H79676± 49719± 55753± 61889± 125982± 941025± 1091338± 152多面体BHRZ03821± 88785± 42854± 139948± 1011078± 881762± 11283008± 13993间隔31± 733± 237± 342± 449± 653± 659± 8八角形626± 275546± 80503± 78560± 67706± 135794± 302720± 12无柄类1429± 51625± 211709± 91996± 302294± 672552± 492942± 70Par−axesH Int4509± 294866± 105455± 295925± 166102± 687030± 1787971± 99多面体H79771± 126758± 90851± 145906± 771049± 1571123± 541248± 33多面体BHRZ03886± 102896± 1261267± 9081011± 1561129± 1321443± 1763017± 1323表5分析的平均执行时间和标准偏差（毫秒）。G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）31314G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）32.4性能在表5中，我们以毫秒为单位显示了分析的执行时间。每个分析都在具有8 GbRAM的Intel Core i5- 2400 K上执行了5次。报告平均执行时间和标准偏差。报告值包括将模型转换为方程组所需的时间和求解所得方程组所需的时间。 它既不包括从磁盘加载模型，也不包括解析。对于间隔和八边形，扩大延迟不会对性能产生很大影响。 对于多面体的两种变体，情况正好相反。 这可能是因为用多面体外壳代替加宽会产生更复杂的多面体，这会严重损害后续抽象运算符的性能。缩小延迟对任何域的执行时间都没有太大的影响。从性能的角度来看，区间、八边形和多面体的执行时间都符合预期。间隔比其他任何东西都快对于加宽延迟的低值，八边形和多面体的速度相当，但是对于延迟的高值，八边形更快。最慢的域是带间隔的重叠域和它们的约化积。虽然这与理论结果形成对比，但实际上这是因为虽然八边形和多面体是PPL的一部分，它是用C++编写的并且高度优化，但平行六面体是用Scala编写的，其函数式风格并不特别适合这种应用程序。实际上，间隔也是用Scala本机编写的，但由于这种情况下的算法非常简单，这可能是一个优势，因为使用PPL中的实现将导致从Java虚拟机调用本机代码的开销。有些结果有很高的标准偏差。这可能是由于Java虚拟机的某些工件，如垃圾收集。3结论我们比较了多面体、区间、八边形、平行六面体以及平行六面体与区间的简化积的相对精度。使用Jandom静态分析器对ALICe基准测试进行区间约束。我们已经证明，虽然多面体域在理论上是推断线性关系最精确的，但在实践中，表达性较低的域可以找到更精确的结果，特别是平行体和区间的约化积我们还表明，延迟加宽通常可以提高结果的精度，直到某个值（约3，4），但标准加宽的多面体域除外，在那里它具有不利的效果。最后，我们已经证明了延迟收缩对分析的精度没有显著影响，除了多面体域，缺少收缩算子，在下降阶段至少需要延迟1才能采取步骤。作为未来的工作，我们计划使用技术进行更多的实验，以提高分析的精度，例如局部加宽和缩小[9]，G. Amato，M. Rubino/电子笔记在理论计算机科学334（2018）3-1615[13][14][15][16][17][18][19]引用[1] Amato，G.，S. Di Nardo Di Maio，M. C. Meo和F. Scozzari，模板抽象域上的窄化运算符，在：N。Bjøner和 F. de Boer，editors，FM 2015：Formal Methods，20th International Symposium，Oslo，Norway ， June 24-26 ， 2015 ， Proceedings ， Lecture Notes in Computer Science9109 ， Springer ，Berlin Heidelberg，2015 pp.57比72[2] Amato ， G. ， S. Di Nardo Di Maio ， M. C. Meo 和 F. Scozzari ， 模 板 抽 象 域 的 下 降 链 和 缩 小 ， ActaInformatica在线（2017），将以印刷版出版。DOI：10.1007/s00236-016-0291-0。[3] Amato，G.，S. Di Nardo Di Maio和F. Scozzari，用Soot进行数值静态分析，见：ACM SIGPLAN国际Java程序分析最新技术研讨会论文集，SOAP’13[4] Amato，G.，M. Parton和F. Scozzari，一个挖掘部分执行跟踪以改进静态分析的工具，在：H。Barringer等人，editors，First International Conference，RV 2010，St. Julians，Malta，November 1-4，2010.Proceedings，Lecture Notes in Computer Science 6418，Springer，Berlin Heidelberg，2010 pp. 475-479[5] Amato，G.，M. Parton和F.Scozzari，通过简单分量分析发现不变量，符号计算杂志47（2012），pp.1533-1560年。[6] Amato，G.， M. Rubino 和F. 斯科扎里， 推断 线性 不变量与 parallelotopes，计算机编程科学在线（2017），将以印刷版出版。DOI：10.1016/j.scico.2017.05.011。[7] 阿 马 托 湾 ， 巴 西 - 地 和 F. Scozzari ， Optimality in goal-dependent analysis of sharing ， Theory andPractice of Logic Programming9（2009），pp. 617-689[8] 阿 马 托 湾 ， 巴 西 -地 和 F. Scozzari ， 平 行 六 面 体 的 抽 象 域 ， 在 ： J. Midtgaard 和 M. Might， editors ，Proceedings of the Fourth International Workshop on Numerical and Symbolic Abstract Domains ，NSAD 2012，Electronic Notes in Theoretical Computer Science287，Elsevier，2012 pp. 17-28.[9] 阿马托湾，巴西-地和F. Scozzari，局部扩大和缩小，在：F。Logozzo和M. Fähndrich，editors，StaticAnalysis.第20届国际研讨会，SAS 2013年，西雅图，华盛顿州，美国，2013年6月20日至22日，会 议 记录，计算机科学讲义7935（2013），pp. 25比42[10] Amato ， G. ， F. 斯 科 扎 里 Seidl ， K. Apinis 和 V. Vojdani ， E. Esciently intertwining widening andnarrowing，Science of Computer Programming120（2016），pp.1-24[11] 巴尼亚拉河P. M.希尔，E. Ricci和E. Za Zaganella，Precise widening operators for convex polyhedra，Science of Computer Programming58（2005），pp.28比56[12] 巴尼亚 拉河P. M. Hill和E. Za Zaghanella，The Parma Polyhedra Library：Toward a complete set ofnumerical abstractions for the analysis and verification of hardware and software systems，Science ofComputer Programming72（2008），pp. 3-21[13] Blanchet，B.，库索河Cousot，J. Feret，L. Mauborgne，A. 米内湾 Monniaux和X. Rival，大型安全关键软件的静态分析器，在：ACM SIGPLAN 2003年编程语言设计和实现会议论文集（PLDI196-207.[14] Cousot，P. and R. Cousot，Static determination of dynamic properties of programs，in：Proceedingsof the Second International Symposium on Programming（1976），pp.106-130[15] 库索山口和N.Halbwachs，自动发现程序变量之间的线性约束，在：POPL84比97[16] Gopan ， D. 和 T. 代 表 ， 前 瞻 扩 展 ， 单 位 ： T 。 球 和 R 。 B. Jones ， editors ， Computer AidedVerification，18th International Conference，CAV 2006，Seattle，WA，USA，August 17-20，2006. Proceedings，Lecture Notes in Computer Science 4144（2006），pp. 452-466[17] Halbwachs ， N.， “Détermination Automatique de Relations Linéaires Vérifoées par les Variables d’unProgramme,”法国格勒诺布尔大学科学与医学博士论文（1993年）。16G. Amato，M.Rubino/Electronic Notes in Theoretical Computer Science 334（2018）3[18] 让内湾和A.Miné，APRON：一个用于静态分析的数值抽象域库，在：A. Bouajjani和O. Maler，编辑，计算机辅助验证，第21届国际会议，CAV 2009，法国格勒诺布尔，2009年 6 月 26 日 至 7 月 2 日 。 Proceedings ， Lecture Notes in Computer Science 5643 ， Springer ， BerlinHeidelberg，2009 pp. 661-667[19] Maisonneuve，V.，O. Herbal和F. Irigoin，Alice：A framework to improve a contrast loop invariantcomputation，in：5th Workshop on Invarian