自动分析递归数据结构的归纳性质

提出了一种对递归数据结构的归纳性质进行自动化分析的框架.工作分为3个主要部分.首先,它将递归数据结构的归纳性质分为两个主要类别,并提出对应的处理模式,从而帮助简化对于程序中的递归数据结构上的相关性质的分析.其次,提出了一种称为分割与拼接的技术来发现和描述递归数据结构是如何被程序修改的:递归数据结构首先被分割为若干个互不相交的片段,然后,这些片段以新的方式重新拼接在一起,形成一个新的数据结构.这个技术的重点在于如何将程序原有的性质保留下来,从而为后面的分析过程所使用.最后,提出了一种调用上下文敏感的程序摘要过程间分析方法.案例分析和实验结果表明:分析框架可以有效地分析递归数据结构的归纳性质,并生成对程序证明过程有用的断言.

常用循环摘要的自动生成方法及其应用

采用形式化方法证明软件的正确性,是保障软件可靠性的有效方法.而对循环语句的分析与验证,是形式化证明中的关键,对循环语句的处理一直是程序分析与验证中的一个难点问题.提出使用循环语句修改的内存和这些内存中存放的新值来描述循环语句的执行效果,并将该执行效果定义为循环摘要.同时,提出一种自动生成循环摘要的方法,可以为操作常用数据结构的循环自动生成循环摘要,包含嵌套循环.此外,基于循环摘要,可以自动生成循环语句的规约,包括循环不变式、循环的前置条件以及循环的后置条件.已经实现了自动生成循环摘要以及循环规约的方法,并将它们集成到验证工具Accumulator中.实验结果表明,该方法可以有效地生成循环摘要,并生成多种类型的规约,从而辅助软件程序的形式化证明,提高验证的自动化程度和效率,减轻验证人员的负担.

自动合成数组不变式

提出了基于抽象解释框架自动合成数组程序不变式的方法,它能够分析按照特定顺序访问一维或者多维数组的程序,然后合成不变式.该方法将性质(包括区间全称量词性质和原子性质)集合作为抽象域,通过前向迭代数据流分析合成数组性质.证明了该方法的正确性和收敛性,并通过一些实例展示了该方法的灵活性.开发了一种原型工具,该工具在各种数组程序(包括competition on software verification中的array-examples benchmark)上的实验展示了方法的可行性和有效性.

通过抽象程序证明复杂具体程序

描述了证明抽象程序和具体程序满足一致性关系的方法.抽象程序使用抽象数据结构(ADTs),如set,list,map及其上的操作.具体程序使用类C语言中的类型.抽象程序和具体程序一致性证明需要用户给出抽象变量和具体变量的关系、抽象程序程序点和具体程序程序点的对应关系.基于对应关系,抽象程序和具体程序一致性证明可以分解,从而容易并可能自动证明.

基于DWT和SVD的数字水印算法

为了使水印算法具有更强的鲁棒性，提出一种基于离散小波变换（DWT）和奇异值分解（SVD）的数字水印算法．在水印嵌入之前首先对其进行调制。利用种子序列按照水印的大小生成一组随机数，并将这组随机数和原始水印图像进行调制．然后将调制后的水印嵌入到原始载体图像的离散小波域中。在水印提取时再利用调制过程的逆过程恢复出水印。实验结果证明了该方法对于JPEG压缩、噪声、旋转、剪切等具有很好的鲁棒性。