线性规划模型检验的扩展及其有效性分析

理论计算机科学电子笔记144（2006）79-94www.elsevier.com/locate/entcs用数组进行线性规划的模型检验亚历山德罗·阿曼多1意大利Genova大学DIST的AI-Lab马西莫·贝内切蒂2文凭diScienzeFisiche，Universita`diNapoliJacopo Mantovani3意大利Genova大学DIST的AI-Lab摘要在以前的工作中，我们提出了线性程序作为命令式程序的细粒度模型，并展示了如何将SLAM中使用的模型检查过程推广到线性程序的模型检查过程。在本文中，我们表明，我们的线性规划的模型检测过程可以扩展到这样一种方式，以支持分析的线性规划具有符号的未定义值和条件表达式。 这一延伸尤为重要 因为它为更广泛类别的命令式程序的模型检查过程的构造铺平了道路，例如，线性程序与数组我们提供了一个详细的说明符号模型检查过程，这类扩展的线性规划，讨论其实现的尤里卡工具，并提出实验结果，确认其有效性的分析，线性程序与数组关键词：软件模型检测，线性约束，数组，线性算术，决策过程1介绍反例引导的抽象细化是软件模型检查的主要方法之一（例如[9，5，14]）。在这种情况下，布尔程序1 电子邮件地址：armando@dist.unige.it2电子邮件：info.benerecetti@ na.infn.it3 电子邮件地址：jacopo@dist.unige.it1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.01.00680A. Armando等人理论计算机科学电子笔记144（2006）79D∗···∗D(i.e.具有通常的控制结构但其变量被限制在布尔值范围内的程序），例如，在SLAM项目[3]中，作为命令式程序的可能抽象，逐渐细化为越来越具体的程序。优点是存在布尔程序的有效模型检查过程（例如[4，12]）。虽然该方法已被证明在特定应用领域（如设备驱动程序编程）非常有效[5，14]，但其在其他更普通的程序类上的有效性 注意，自从检测到虚假执行跟踪导致检查和细化循环的新迭代，该方法的效率以关键的方式取决于抽象程序所允许的虚假执行跟踪的数量。当然，抽象越接近原始程序，可能需要分析的虚假执行跟踪的在以前的论文[2]中，我们提出了线性程序作为命令式程序的细粒度模型，并展示了如何将SLAM中使用的模型检查过程推广到线性程序的模型检查过程。线性规划不同于布尔规划，因为规划变量可以在数值域（例如Z或R）上变化;此外，所有条件和变量赋值都涉及线性表达式，即。形式c0+c1X1++ C nxn，其中c0，...，c n是数字Z和x1中的常数，...，x n是程序变量，. 线性程序可以显式地编码数据和控制之间的复杂相关性，这些相关性在使用布尔程序时必须被抽象掉在本文中，我们表明，我们的线性规划的模型检测程序可以扩展到这样一种方式，以支持分析广义线性规划，即。线性规划的特征在于（i）未定义值的符号和（ii）条件表达式。这种扩展是特别重要的，因为它为更广泛的命令式程序的模型检查过程的构建铺平了道路，例如，线性程序与数组本文件的结构如下。在第2节中，我们通过一个例子展示了如何通过使用模型检查器作为黑盒对广义线性规划进行模型检查在第3节中，我们定义了广义线性规划的语法和语义。在第4节中，我们提供了一个详细的说明广义线性规划的符号模型检查程序。在第5节中，我们讨论了我们的想法在EUREKA[2]工具中的实现，并给出了初步的实验结果，证实了它们的有效性。A. Armando等人理论计算机科学电子笔记144（2006）79812用数组进行我们的方法来模型检查线性程序的数组是基于抽象出所有数组元素从初始程序的想法，然后增量细化所产生的抽象程序，包括数组元素的建议，由细化过程。PP=0第1页void main（）{void main（）{public voidrun（）{int i，a[3];整数i;int i，a = 1;[1]int [1]nums = 1;[1];[1]a1=（1==1）？1：u;[2]i=0;[2]i=0;[2]i=0;[3]while（a[i]！1 i 3）[3]while（u！1&&i< 3）[3]while（（i==1）？a1：u）！=1 i 3）&&[4]美国{a[i]=2*i;[4]美国{;[4]{a1=（i==1）？2*i：a1;[5]i=1;}[5]i=1;}[5]i=1;}[6]if（i>1）[6]if（i>1）[6]if（i>1）[七]《中国日报》错误：;}[七]《中国日报》错误：;}[七]《中国日报》错误：;}图1.一、 一个抽象程序（P），初始抽象（P0）和它的精化（P1）。设P是图1中的线性规划。我们首先抽象Pi n来编程Pin0，方法是用符号u（表示数值类型的任意值）替换每个数组表达式的发生，并用skip语句（;）替换每个数组元素的赋值。然后，将线性规划的模型应用于P_0，以确定使用ERROR标签标记的行的可达性。 轨迹1，2，3，4，5，3，4，5，3、4、5、3、6、7被模型检查器检测到。(How这一点在以下各节）。这个跟踪对应于执行while循环的三次迭代（第[3]因此，第[6]行if语句的条件计算为true，最终到达标记为ERROR上述跟踪w.r.t. P是通过生成一组公式，其令人满意的估值对应于所有可能的执行序列的声明P对应的跟踪正在审议。这是通过首先重命名出现在语句中的变量，这样在执行过程中没有变量被赋值两次（如[8，10]中所做的），然后通过生成对重命名语句的行为进行编码的公式来完成的。表1显示了原始语句、重命名语句和上面跟踪的关联公式的序列。由此产生的一组公式然后被馈送到定理证明器。 如果82A. Armando等人理论计算机科学电子笔记144（2006）79∈∪ ∩∅D {}联系我们如果发现它是不满足的，那么跟踪在P中是不可执行的，而如果发现它是满足的，那么我们可以得出结论，跟踪在P中也是可执行的。在我们的例子中，我们发现这组公式（见表1最右一列）是不令人满意的。有助于证明不满意性的公式是与步骤1、2、4、5和6相关的公式。请注意，a4[i5]项（上下文中给出了i5= 1）出现在关联的公式步骤6。这意味着，为了排除上述迹，我们必须通过包括位置1处的元素来精化P 0，从而获得P1。在一般情况下，如果k1，…，k n是要包含的数组a的索引在细化的程序中，然后细化步骤相当于替换每个形式a[e]的表达式与条件表达式（e==k1？ ak1：（e==k2？ ak2：.. .（e==kn？akn：u），然后每个赋值为a[e1]=e2的形式;具有（并行）赋值ak1， . ，akn=（e1==k1？ e2：ak1）， . ，（e1==kn？e2：akn）;其中k1， . ，akn是对应于要包括在细化程序中的不同数组元素的数字类型的新变量。(If n=0，上面的赋值简化为一个skip（;）语句。的应用线性规划问题的数学模型表明，在第1页中无法实现这一陈述，因此我们可以得出结论，错误语句在P中不可达。上述抽象技术及其基本属性的技术介绍可以在[1]中找到3线性规划与线性数组规划设W是一组程序变量。令V ={v1，...，Vl} Vw是一组程序变量，范围为设A=a1，.，am我们是一套数组变量一个数组变量a A是一个程序变量，配备了一个正整数dim（a），数组的大小。集合A和V形成W的一个划分，即W=VA和VA=。 此外，让你成为一个独特的符号代表未完成。广义（布尔型）集合E（B）带数组的线性表达式（以下简称为带数组的线性表达式）由以下BNF产生式规则定义：E：：= u |Z |V |Z * E |E + E|（B？英：英）|A[E]B：：=（E op E）其中op>=，=<，<，>，==，！= . 没有数组的广义线性（简称线性表达式）的定义包含在上面。在A. Armando等人理论计算机科学电子笔记144（2006）7983步骤线原创声明重命名语句式1 [1]第一章int [1] nums =1;1[1] = 1;a1=store（a0，1，1）2 [二]《中国日报》i= 0;return0;i2= 03 [3]第一章假设（a[i]！=1i 3）;假设（a1[i2]！=1i23）;a1[i2]/=1i234 [4]美国int[i]= 2 *i;a4[i2]=2 *i2;a4=store（a1，i2，2i2）5 [五]《中国日报》i=i+1;i5=i 2+1;i5=i2+ 16 [3]第一章假设（a[i]！=1i 3）;假设（a4[i5]！=1i53）;a4[i5]/=1i537 [4]美国int[i]= 2 *i;a7[i5]= 2 *i5;a7=store（a4，i5，2i5）8 [五]《中国日报》i=i+1;i8=i 5+1;i8=i5+ 19 [3]第一章假设（a[i]！=1i 3）;假设（a7[i8]！=1i3）;a7[i8]/=1i8310 [4]美国int[i]= 2 *i;a10[i8]= 2 *i8;a10=store（a7，i8，2i8）11 [五]《中国日报》i=i+1;i11=i 8+1;i11=i8+ 112 [6]美假设（！（a[i]！=1i 3））;假设（！（a10[i11]！（a10[i11]/=1i113）84A. Armando等人理论计算机科学电子笔记144（2006）79D国=1i113））;13 [6]美国return（i）;return（i）;i11>1表1检查追踪的可行性。下面，EW将表示W上具有数组的线性表达式的集合。线性程序（带数组）是一个具有通常的控制流结构（if，while，assert）和过程抽象的程序，具有按值调用参数传递和递归。变量范围超过 此外，所有条件和变量赋值都涉及线性表达式（分别用数组）。我们表示的数值变量和数组变量的集合P分别与VP和AP我们假设每次出现（！b1）、（b1&&b2）和（b1||b2）在程序中被等价的表达式（b1？0：1），（b1？b2：0），（b1？1：b2）分别。此外，每一个布尔线性表达式b发生-环外的保护条件表达式，被替换为以下等价的线性表达式（b？1： 0）。因此，在重写之后，布尔表达式将只出现在条件表达式的保护内。我们还假设在原始程序中的每个过程调用之后立即添加skip语句（;）。通过这种方式，过程调用的返回点是唯一的、显式的，并且在程序的控制流程图中被标记。最后，与[4]一样，在不失一般性的情况下，我们假设所有变量名和语句标签都是全局唯一的。程序P的控制流程图是有向图GP=（NP，SuccP），A. Armando等人理论计算机科学电子笔记144（2006）7985∪∩⟨⟩联系我们∈ {−}DCITD其中NP=0，1，.，n，n +1，n + p是顶点集4，Succp：NP2NP映射每个顶点在其后继顶点集上. 对于任何满足1≤i≤n的顶点，si表示与i对应的程序语句。如果s i是if（e）、while（e）或assert（e），则Succ P（i）={Tsucc P（i），Fsucc P（i）}，其中Tsucc P（i）（Fsucc P（i））表示当e评估为真（分别为假）时i的后继。如果s i为assert（e），则Fsucc P（i）=0。 如果pr是P中的一个过程，那么First P（pr）是pr中第一个语句对应的顶点，而ExitP（pr）是pr的出口顶点。 如果si是一个pr（i），则Succ P（i）={First P（pr）}，RetPt P（i）是紧跟着过程调用的; state的顶点.此外，如果s i是在过程pr的主体中发生的状态，则ProcOf P（i）=pr。如果s i是过程pr中的返回语句，则Succ P（i）={Exit P（pr）}，并且Succ P（Exit P（pr））={j∈N P：s i=pr（e）;并且j=RetPt P（i）}。最后，如果Succ P（i1）={i2}，我们定义sSucc P（i1）= i2。 我们还假设存在一个称为main的过程，并且First P（main）= 1。给定一个程序P，GlobalsP表示P的全局变量集，对于任意i∈NP，FormalsP（i）是包含i的程序的形式参数集，LocalsP（i）是顶点作用域中的局部变量集I. 此外，我们定义InScopeP（i）= GlobalsP LocalsP（i）。设W是一组程序变量，W上的赋值ω是一个全函数，它将V W 中 的数值变量映射到，每个数组变量AW映射到从0，. 调（a）1 到.一个线性规划的状态是一个对i，ω，其中i是P的控制流图的顶点，ω是W在P（i）上的赋值.因此，ω是InScopeP（i）上的全函数。线性规划的状态定义包含在上面的定义中。我们将ω提升为全函数ω：EW−→2D，4从1到n的顶点与程序语句相关联，顶点0模拟断言语句的失败，从n+1到n+p的顶点是86A. Armando等人理论计算机科学电子笔记144（2006）79⎧⎪否则，D/єєD → D⟨ ⟩ ⟨⟩如果e=a[e1]，则{d∈ω（a）（d1）：d1∈ω（e1）}⎪11P2ω（e1）<$ω（e2）如果e =（b？e1：e2）和{0，d}<$ω（b）2线性表达式与数组定义如下：{e}如果e ∈Z{ω（e）}如果e∈V且ω（e1）∈ {0，.，dim（a）− 1}⎪{c·d1：d1∈ω（e1）}如果e=c*e1ω（e）=n∈{d1opd2：d1∈ω（e1）andnd2∈ω（e2）}如果e=e1ope2其中op ∈ {>=，=<，<，>，==，！= ，+}⎪对于某个d/= 0⎪ω（e1）如果e =（b？e1：e2）和0/∈ ω（b）当e =（b？e1：e2）和ω（b）={0}直觉上，ω（e）是所有与ω相容的e值的集合。表达式e中所有出现的u符号，以及那些对应于数组越界访问的符号，都是通过非确定性地将任意元素分配给相应的子表达式来建模的。 ω以明显的方式被扩展到表达式的kP中的状态跃迁记为yi， ω−→σi， ω，其中σ是符号或形式为CALL（i，ω）或RET（i，ω）的表达式，其中i∈ N P，使得存在过程调用s j，i=RetPt（j）且ω：Locals P（j）→ D（形式为CALL（i，ω）和RET（i，ω）的终端分别表示s j调用的过程的入口点和出口点）。我们使用粗体字母如x来表示变量、元素或表达式的向量W也是所有的f或平行指派，表示为yx=ei。 更进一步，令c=c1，c2，.，c n和d=d1，d2，.，d n分别是集合X和中的n个值元组; f或一个函数f：X b y f [ d / c ] w e表示函数fJ使得f J（c k）= d k，对于所有k = 1，2，.， n，且f J（c）= f（c），对于所有c = c k并且k = 1，2，.，n.程序P的状态转换定义如下：• 如果si1是一个skip（;）或一个returnstatement，则ωi1，ω1<$−→P<$sSuccP（i1），ω1<$;• 如果si1是一个平行分配y=e，则i1，ω1对于d∈ω1（e）;A. Armando等人理论计算机科学电子笔记144（2006）7987єєσ2σn0⟨ ⟩ ⟨ ⟩ ⟨ ⟩ ⟨⟩0PPnn00Pnn• 如果si1是一个赋值a[e1] =e2，则<$i1，ω1<$−→P<$sSuccP（i1），ω1[（ω（a）[d2/d1]）/a]<$，对于d1∈ω1（e1）和d2∈ω1（e2）;• 如果si1是形式为if（e）、while（e）或assertt（e）的状态，则i1，ω1其中，当0∈ω1（e）时，i2=FsuccP（i1），当d∈ω1（e）时，i2=TsuccP（i1）;• 如果si1=pr（e），则CALL（RetPtP（i1），ω）i1，ω1其中ω：局部域P（i1）→ D使得ω（x）=ω1（x），ω2（y）∈ω1（e），并且ω2（g）=ω1（g）其中x=局部P（i1），y=形式P（i2），g=整体P;• 如果i1是pr的出口顶点，则RET（i2，ω）i1，ω1其中i2∈SuccP（i1），ω2（g）=ω1（g），对所有g=全局P，ω2（x）=ω（x），对所有x=局部P（i2）.程序P的p路是s序列<$i， ω<$−σ→1i， ω···−→i，ωσk+10 0P1 1PPn n对k=0， ... ， n−1。（在续集中，σn将把i， ω−σ→1· · ·−→i， ω与i， ω−σ−1−···−σ→ni， ω进行交换。）不-注意，并非所有路径都代表潜在的执行路径：在像RET（i2，ω）其中i1=退出pr，估值ω可以选择arbi，因此，ω2不能保证与调用者的局部变量ω1一致，这是过程调用的语义所要求的从i0，ω0到in，ωn的有效路径描述了通过一系列执行步骤从i0，ω0到in，ωn的传输，在此期间，调用堆栈可能会暂时变深（由于过程调用），但永远不会比其原始值浅深入初始化路径是初始状态为ω 1，ω0为ω0的路径。一个状态<$i，ω<$i是可达的当且仅当存在一条初始化的有效路径到i，ω。 顶点i∈NP可达当且仅当存在赋值，故能得之，故能得之。88A. Armando等人理论计算机科学电子笔记144（2006）790e联系我们→P规则：4线性规划的符号模型检验我们的模型检查过程扩展了[4]中描述的模型检查过程，这反过来又是Reps，Horwitz和Sagiv在[17]中定义的制表算法的改编。5设i∈NP，e是与第一个语句相关联的节点，包含s的过程i. 入射到i中的路径边πi=<$ωe，ωi <$是一对证明了存在valid路<$1， ω<$−σ−1−···−σ→k<$e，ω<$−σ−l·−··−σ→m<$i，ω<$i，P i对于某些赋值ω0和0 ≤k≤l≤m.换句话说，路径边表示从ω 1，ω0 ω1到ωi，ω i ω 2的有效路径的子集。对于程序控制流中的每个节点i，我们的过程逐渐建立了i中附带的路径边集的符号表示。语句si的可达性归结为检查i中附带的路径边的集合是否不为空。我们分三个阶段提出这个过程：我们从定义线性算术的公式开始，对并行赋值的语义进行编码（即，α（y，e））和线性经验（即β+（e）和β抽象的析取线性约束），我们用来象征性地表示集合的路径边;最后，我们提供了一个抽象的表征我们的模型检查过程作为一个（归纳定义）的关系在NP-索引的抽象析取线性约束的家庭。设e和ne是线性表达式，B是一组原子布尔线性表达式.我们定义关系e→（B，ne）为最小关系，使得对所有e∈V<$Z<${u}，e→（B，ne）为最小关系，并且在以下推论e1→（B1，ne1）e1→（B2，ne2）如果op*，+，>=，=<，<，>，==，！=（e1ope2）→（B1B2，（ne1opne2））b→（B，nb）e1→（B1，ne1）（b？e1：e2）→（B<$B1<${nb+}，ne1）b→（B，nb）e2→（B2，ne2）（b？e1：e2）→（B<$B2<${nb−}，ne2）其中b+（b−）isb！= 0（b==0，分别） 如果b是线性表达式，且b（！（b）如果b是布尔表达式。可以证明，如果e（B，ne），则线性表达式ne和线性表达式的集合B都不包含条件。设U是一个无穷多个变量的集合，使得U ≠V = V。如果e是线性的[5]为了简洁起见，我们在这里描述一个简化版本的过程，它没有使用汇总边，即：高速缓存过程调用分析结果的数据结构，从而避免后续计算中的冗余工作A. Armando等人理论计算机科学电子笔记144（2006）7989∃∃∃.∃ ⊥表达式中，我们用e表示从e得到的表达式，将每次出现的！b，e1！= e2和e1==e2，分别具有<$b、<$（e1=e2）和e1=e2，并且u在e中的每次出现都具有不同的变量，联合如果w是一个公式，u1，...，u k是U中出现在w中的变量，用U. w表示公式u1.... 英国注意，如果e是一个没有条件的线性表达式，那么e是线性算术语言的表达式。设y和e是变量的k-元组和k >0的线性表达式，使得y中的变量不出现在e中。我们定义Kα（y，e）=i=1.你好。（yi=nei）Bi）水：e i→（B i，ne i），其中i =1，.，k.此外，对于线性表达式e，我们定义β+（e） ={U. （ne+<$B）<$：e→（B，ne）}β-（e）= {\displaystyle {\frac {U}}}。（ne−<$B）n：e→（B，ne）}。例如，如果e=（3 *x +（y<0？u：y）），则e→（{y<0}，3 *x+u）并且e→（{！y<0}，3 *x+ y）。因此，α（z，e）=（u1. （y0<$z=3<$x+u1）<$（<$（y0）<$z= 3<$x+y）），它可以简化为逻辑等价的公式（y0<$（<$（y 0）<$z=3<$x+y））。 类似地，β+（e）=（u1.（y0<$$>（3<$x+u1= 0））<$（<$（y0）<$$>（3<$x+y=0），可以简化为（y0 <$（<$（y0）<$$>（3<$x+y=0）。设e是一个表达式，我们用eJ表示从e得到的表达式，用相应的素数版本（即vJ）替换每个变量，比如v这种符号以明显的方式扩展到表达式的集合（元组）上，即 EJ={eJ：e∈E}（eJ=eJ1， . ，eJn n，如果e=1， . ，例如，分别地）。析取线性约束D（简称DLC）是一个公式，D=我联合jcij，其中cij是线性约束。 符号代表一个不可满足的线性约束。n元抽象析取线性约束（简称ADLC）是λx.λxJ.D形式的表达式，其中D是一个DLC，x是一个n元组，包括D中出现的自由变量。6我们在DLC上定义了以下操作：- 应用程序. 设λxx， J，D是n元的ADLC，s和t是n元线性表达式的元组.δ=λxxJ.D在（s，t）中的应用，符号为δ（s，t），是通过同时将D中x（xJ）中的变量替换为s（tresp.）中的相应元素而[6]在等式中，我们将用λ xx ′来表示eλx.λx′.D。D.90A. Armando等人理论计算机科学电子笔记144（2006）79HJJ- 合取与析取。设D1和D2是DLC，则D1HD2和D1D2分别是逻辑上等价于D1D2和D1D2的任何DLC. 这些操作如下扩展到ADC。 设δ1和δ2是相同元数的ADC，则δ1Hδ2= λxxJ。（δ1（x，xJ）Hδ2（x，xJ））和δ1Hδ2= λxxJ。（δ1（x，xJ）Hδ2（x，xJ））。- 量化消除。 设D是一个DLC，则X = X。D是通过从D中消去x中的变量而得到的与D等价的任何DLC。- 蕴含。设δ1和δ2是相同元数的ADLC，则δ1±δ2i =所有满足δ 1的赋值对也满足δ2，即[δ1]][[δ2]]，其 中 [δ]]={ω ， ωJ ： |=ω<$ωJδ（ x， xJ ） ， ω ：V→D，ωJ：VJ→D}。我们用A（P）表示 NP-指标的ADLC集族，使得 Ai（P）是元的ADLC集，|InScope P（i）|对所有i ∈ NP. 设A（P）7，我们将二元关系定义为： 设i ∈ NP，n= n，j对于所有j/∈SuccP（i），且• 如果i对应于skip（;）或return语句，则1sSuccP（i）=成功率P (i) 夏威夷语• 如果i对应于赋值y=e，则1sSuccP（i）=成功率P（i）H λxxJJ. J.（H_i（x，xJ）H_α（yJJ，eJ）H_zJJ=zJ），其中x=InScopeP（i），z=InScopeP（i）\y;8• 如果i对应于if（b），而e（b）或assert（b）声明t，则1TsuccP（i）∆1=TsuccP= F成功（i）HλxxJ. （αi（x，xJ）Hβ+（bJ）），（i）H λxxJ. （αi（x，xJ）HβFsuccP（i）P其中x= InScopeP（i）;• 如果i对应于过程调用pr（e），则1sSuccP（i）=sSuccP（i）Hλw w′′。（x′. （i（x，x′）Hα（y′′，e′）Hg′′=g′）Hw=w′′），其中x= InScopeP（i），y= FormalsP（pr），w= InScopeP（sSuccP（i）），g= GlobalsP，l= LocalsP（sSuccP（i））;• 如果i是pr的出口顶点，则1=你好。（？k（w，w′ ′）Hy′′=y′′H<$x′z′′. （i（x′，x′′）Hα（f′，e′′）Hg′=g′′）[7]对于每个i∈NP，我们用一种错误的符号表示，对于n∈Ai（P），我们写n∈ A（P）。[8]我们求出x′1 = x1. 其中x′= x，其中x =<$x1，.，x n= 0。∆∆∆∆A. Armando等人理论计算机科学电子笔记144（2006）79911我如果j∈SuccP（i）和k使得sk=pr（e）和RetPt（k）=j，则w=InScopeP（k），y= LocalsP（k），x= InScopeP（i），z=LocalsP（i）。例如，设s i为并行赋值y 1，y 2=（（y 1> 0）？ y 1+ 1：u），y 2+ 1且InScopeP（i）={x，y1，y2}。因 此 ，e = n（（y1> 0）？ y1+ 1：u），y2+ 1，y =y=1，y=2，z=1，x =1，那么，α（yJJ，eJ） =（（y1J J=y1J+1<$y2J=y2J+1<$y1J>0）u1. （y1J=u1y2JJ=y2J+1<$y1J>0））。这可能意味着α（yJ J，eJ）=（（y1JJ=y1J+ 1y1J>0））。因此，被添加到AusSuccP（i）的新的路径边集合由以下ADLCλx，y1，y2，xJ J，y1JJ，y2J J表示。xJ，y1J，y2J. （i（x，y1，y2，xJ，y1J，y2J）H（（y1JJ=y1J+1y2JJ=y2J+1y1J>0xJJ=xJ）（y2JJ=y2J+1y1J>0xJJ=xJ）。作为另一个例子，假设si是语句if（y>0 y == 2*u），+J JInScope P（i）={x，y}，则（经过一些简化）β（b）=u1。（y>0yJ= 2 u1）和β-（b j）= u 1。（yJ>0<$$>yJ = 2<$u1）<$$>（<$yJ>0）。新一组路径边，添加到TsuccP（i）（添加到FsuccP（i），特别是） 由以下ADLC λx.xJ.y.yJ表示。1. （λ i（λx，y∈，λxJ，yJ∈）H（yJ> 0 λ yJ= 2 λu1λ xJ=x ） ） （ λx.xJ. y. yJ 。 1. （ 分 别 为 H （ （ yJ>0 ） <$<$yJ=2<$u1<$xJ=x）<$（<$yJ> 0 <$xJ= x）。设A（P）∈A，我们定义[[]]为NP下面的结果说明了我们的程序的正确性的证明在[1]中可用。设λ0∈ A（P），使得λ0= λxxJ. （xJ=x），x= InScopeP（1）和λ0= λxixJi。其中xi= InScopeP（i），对于所有i ∈ NP\{1}。定理4.1设φ0定义如上。 以下事实成立：i是当且仅当re存在且满足<$0<$$> 1且[[<$1]]/=0时，r e可达到。Di5实施和实验结果本文将线性规划的模型检验方法推广到EU-REKA[2]沿着第4节中讨论的路线，以便它现在支持用u符号和条件表达式扩展的线性规划分析Ssions。量化消除是通过傅里叶-莫茨金方法实现的[16]。蕴涵检查是通过使用ICSv2.0[11]作为线性算术约束的布尔组合的决策过程来完成的。这是通过减少确定δ1±δ2是否保持的问题来实现的，确定公式δ1（c，cJ）的不满足性，其中δ1和δ2是元数为n的ADLC，c是不同常数的n为了评估方法的有效性，我们还在EU-REKA中开发了一个反例引导抽象的原型实现92A. Armando等人理论计算机科学电子笔记144（2006）79第2节中概述的细化程序。为了检查编码模型检查器生成的迹线的可行性的公式的满足性（见第2节），我们使用CVC Lite [6]，因为它是数组理论和线性算术的结合的完整证明。初步实验证实了所提出的方法的有效性。例如，EUREKA很容易得出结论，图1中的程序是安全的。非常有趣的是，Blast [14]（它确实支持数组并实现了惰性布尔抽象）错误地报告了同一个程序是不安全的。原因在于，在Blast中（就像在C语言中一样），a[i]是*（a+i）的简写，并且Blast对任何“[...]表达式p+i，其中p是一个指针，i是一个整数，产生一个指针值，指向p这意味着在分析期间，所有数组元素对于Blast都由于SLAM以相同的方式处理指针，我们希望它应该表现出相同的行为，但我们无法验证这一点，因为SLAM工具包不是公开的。在其他线性程序与数组（成功分析尤里卡）爆炸报告错误，由于无法发现新的谓词的抽象。我们还比较了尤里卡与CBMC [15]。CBMC的核心是一个将C程序的（有界）验证问题编码为SAT公式的过程。CBMC生成的SAT公式中命题变量的数量与此相反，eureka通过以增量和反例驱动的方式考虑数组元素，在许多情况下使用的时间和内存资源与输入程序中定义的数组大小无关。 (The图1中的程序就是一个典型的例子。）更一般地说，我们在许多使用数组的C程序上测试了EUREKA、Blast和CBMC，并将其用作EUREKA的回归测试。结 果 总 结 见 表 2 。10 读 者 可 参 考 EU-REKA 项 目 网 页 （ URL ：http://www.ai.dist.unige.it/eureka）以获得实验结果的详细描述数组越界属性-这里没有显示错误，但很容易看出，对于任何a∈A和e∈E，可以通过在每次出现a[e]之前放置assert（edim（a））（e>= 0）来检查代码。

下载后可阅读完整内容，剩余1页未读，立即下载