一个基于两区间八边形约束的抽象域

抽象解释静态程序分析技术用来发现运行时错误,保证程序正确性,已经被成功应用到工业界。抽象域是抽象解释理论中的一个重要方面,然而大部分已存在的数值抽象域无法表示程序的非凸性质,抽象域的这种凸性限制很多时候会影响数值分析的精度,甚至带来更多误报。基于两区间八边形约束,提出了一个新的数值抽象域,其约束形式为x±y∈[a,b]∪[c,d],其中x和y表示变量取值,a,b,c,d∈R。该抽象域的域元素是用两区间八边形约束表示,因此可以表达某类非凸性质,表达能力强于经典的八边形抽象域,并且相对于八边形抽象域,域操作的计算复杂度并没有提高太多。     

单变量区间线性不等式抽象域

程序变量的值范围信息对于编译器优化、程序分析与验证等应用至关重要.抽象解释理论提供了一种通用框架为程序变量计算近似的但是可靠的值范围.然而该框架下已有的数值抽象域在表达非凸性质方面存在一定的局限性,影响了值范围分析的精度.文中基于抽象解释理论,提出一个新的数值抽象域——单变量区间线性不等式抽象域.其主要思想是使用单变量区间线性不等式约束作为域元素的约束表示方法.该抽象域的表达能力强于经典的区间抽象域,并允许表达某类非凸、非连通性质.同时,其域操作存在高效的实现算法.该抽象域具有很强的可扩展性,能够应用在实际大规模的程序分析中.     

基于区间向量抽象域的数值程序分析算法

为权衡对矩阵运算静态分析的精度和效率,针对程序中表示矩阵的变量,提出一种基于抽象解释的抽象与分析算法,即区间向量抽象域。将矩阵变量抽象为一个区间向量对,即行区间向量和列区间向量,矩阵各元素的值范围是由这两个区间向量对应元素的交集表示;设计在该抽象域上的操作以及迁移函数。通过对区间向量抽象域的计算,较好地权衡矩阵元素值范围分析的精确度和分析效率。实验结果表明,该抽象域能够较精确地分析程序中矩阵各元素的值范围,与现有的分析数组的抽象域相比,在分析精度和效率之间取得了合理权衡。     

含有析取语义循环的不变式生成改进方法

抽象解释为程序不变式的自动化生成提供了通用的框架,但是该框架下的大多数已有数值抽象域只能表达几何上是凸的约束集.因此,对于包含(所对应的约束集是非凸的)析取语义的特殊程序结构,采用传统数值抽象域会导致分析结果不精确.针对显式和隐式含有析取语义的循环结构,提出了基于循环分解和归纳推理的不变式生成改进方法,缓解了抽象解释分析中出现的语义损失问题.实验结果表明:相比已有方法,该方法能为这种包含析取语义的循环结构生成更加精确的不变式,并且有益于一些安全性质的推理.     

单元自动化测试中类的抽象内存模型研究

由于面向对象程序具有多态性等复杂特性,在软件单元测试中仅凭静态分析难以判断指针和引用指向对象的具体类型,为了解决这一问题,对类的抽象内存模型进行研究,并提出类的操作语义模拟算法;在路径分析时,通过构建和更新抽象内存模型,从而对变量所属类的范围进行限定;对于单元测试,对基于输入域的随机测试进行优化,提出基于路径的随机测试方法,得到输入变量的类型集合;实验表明,类的抽象内存模型结合操作语义模拟算法能够有效提取出路径中类相关的约束,基于路径的随机测试方法比起基于输入域的随机测试方法能够明显提高测试效率。     

C程序非法计算缺陷的静态检测

为实现基于静态分析技术自动的检测C程序中的非法计算缺陷,提出了一种基于区域内存模型进行非法计算缺陷检测的方法。对C程序中的非法计算缺陷操作归纳总结出其受限集,以对相应运算进行约束;通过抽象的区域内存模型表示实际的内存存储,实现了基于抽象内存区域内存模型的数据流分析;基于数据流分析的结果,判定C程序中的受限操作是否违背受限集的约束,以实现非法计算缺陷的检测。5个实际工程的检测结果分析表明,该方法可有效地检测出C程序的各类非法计算缺陷。     

基于抽象凸估计选择策略的差分进化算法

针对传统差分进化算法计算代价、可靠性及收敛速度的问题,提出一种基于抽象凸估计选择策略的差分进化算法(DEUS).首先,通过提取新个体的邻近个体建立局部抽象凸下界松弛模型;然后,利用下界松弛模型估计目标函数值来指导种群更新,同时利用下界估计区域极值点快速枚举算法系统排除部分无效区域;最后,借助线性拟凸包络的广义下降方向有效地实现局部增强.12个标准测试函数的实验结果表明,所提算法计算代价、可靠性及收敛速度均优于DE及DERL,DELB,Sa DE等改进算法.     

基于完备抽象解释的模型检验CTL公式研究

在模型检验中,抽象是解决状态空间爆炸问题的重要方法之一.给定具体Kripke结构和时序描述语言CTL,基于抽象解释框架以及完备抽象解释和性质强保留之间的关系,抽象模型最小精化使得CTL性质强保留,可转换为抽象解释中抽象域的最小完备精化,并且总是存在抽象域的最小完备精化.根据状态标签函数确定初始抽象域,然后通过不动点求解,获得对CTL标准算子完备的最小抽象域,并依据此抽象域求得CTL性质强保留的最优抽象状态划分,最后构造出CTL性质强保留且最优的抽象状态转换系统.并指出了抽象域对CTL标准算子是完备的当且仅当抽象域对补集和标准前向转换是完备的.     

基于指向与数值抽象的带指针算术程序的分析方法

带指针算术的程序往往包含数组越界、缓冲区溢出等运行时错误。单纯的指针分析技术和数值分析技术都无法有效处理指针算术。为了将指针分析与数值分析相结合,首先提出一种新的指针内存模型,然后基于该模型设计了一个刻画指针指向关系和指针偏移量的抽象域。最后在抽象解释框架下,设计并实现了一个面向带指针算术C程序的静态分析工具原型PAA。实验结果表明,PAA能够有效地分析指针程序的指向关系和数值性质,并能够在效率和精度间取得合理的权衡。     

基于符号模拟和约束逻辑编程的RTL级Verilog谓词抽象方法

利用人工智能最新研究成果--约束逻辑编程对Verilog描述进行谓词抽象,并与目前基于SAT的方法进行了比较.首先通过符号模拟建立Verilog的形式化模型,然后结合要抽象的谓词,将谓词抽象问题转化为约束逻辑编程问题并进行求解.该方法的优点是在计算抽象系统时,不需要像基于SAT的方法那样将字级约束打散成位级约束,求解效率显著提高;提供了一个统一的框架用于描述各种约束.实验结果表明,与基于SAT的抽象技术相比,基于约束逻辑编程的抽象方法的求解速度有显著提高.     

MESHJOIN*:实时数据仓库环境下的数据流更新算法

提出了一种新的实时数据仓库环境下的数据流更新算法——MESHJOIN*算法。算法的特性有:(1)关系R采用了分块和散列的组织形式,尽可能避免对当前连接无效元组的读取,减少连接操作所涉及元组的数量,从而提高连接算法的效率;(2)采用了多线程并发连接技术,并根据工程学原理,实现了连接操作和关系R读取操作的最佳调度,保证了连接算法效率的最大化;(3)根据当前系统的服务率和数据流元组的到达率之间的关系,合理调度实时元组和准实时元组的执行,保证了系统对实时元组的处理要求。实验结果表明,MESHJOIN*算法可以取得比MESHJOIN算法更好的性能。     

基于双群双域四向水平倾角最小化圈绕的凸壳并行新算法

本文针对现行凸壳算法(诸如:串行类的卷包裹凸壳算法、格雷厄姆凸壳算法等,并行类的折半分治凸壳算 法、快速凸壳算法等)效率不高的缺点,根据同构化凸壳构造基本定理,利用工作站机群优点,提出了效率更高的双群(即:其机群分为2个子机群)、双域(即:其数据分布域分为2个子分布域)、四向(即:其每个子分布域内凸壳顶点的寻找方向均各自为顺时针、逆时针2个寻找方向)水平倾角最小化圈绕的凸壳并行新算法.     

Exact and efficient construction of Minkowski sums of convex polyhedra with applications

We present an exact implementation of an efficient algorithm that computes Minkowski sums of convex polyhedra in R³. Our implementation is complete in the sense that it does not assume general position. Namely, it can handle degenerate input, and it produces exact results. We also present applications of the Minkowski-sum computation to answer collision and proximity queries about the relative placement of two convex polyhedra in R³. The algorithms use a dual representation of convex polyhedra, and their implementation is mainly based on the Arrangement package of Cgal, the Computational Geometry Algorithm Library. We compare our Minkowski-sum construction with the only three other methods that produce exact results we are aware of. One is a simple approach that computes the convex hull of the pairwise sums of vertices of two convex polyhedra. The second is based on Nef polyhedra embedded on the sphere, and the third is an output-sensitive approach based on linear programming. Our method is significantly faster. The results of experimentation with a broad family of convex polyhedra are reported. The relevant programs, source code, data sets, and documentation are available at http://www.cs.tau.ac.il/~efif/CD and a short movie [Fogel E, Halperin D. Video: Exact Minkowski sums of convex polyhedra. In: Proceedings of 21st annual ACM symposium on computational geometry. 2005. p. 382-3] that describes some of the concepts portrayed in this paper can be downloaded from http://www.cs.tau.ac.il/~efif/CD/Mink3d.avi.     

基于直方图的并行结构连接算法

连接操作是最昂贵且常用的数据库操作．在传统数据库系统中，主要的连接操作是等值连接操作，因此，传统的并行连接算法主要集中于并行等值连接操作．另外，随着XML在Web应用中变得越来越重要，XML已经成为Internet上一种新的数据交换标准．对XML数据的连接操作不同于传统数据库中的等值连接操作，它属于结构连接操作．以前适合等值连接操作的并行连接算法并不能有效地解决结构连接问题．因此，第1次提出了并行结构连接问题，并且通过应用直方图的思想于并行连接中，从而提出两种基本的并行XML结构连接算法、等高直方图连接算法和等宽直方图连接算法．实验表明这两种算法具有较好的性能．     

一种平面点集凸包与三角网格综合生成的算法

平面点集作为一种觉数学模型,其上常做的运算是求其凸包和三角网格,目前二者的研究是独立进行的,鉴于在很多情形下这两种处理结果均需要,提出了一种综合算法：在对离散点集进行ｄｅｌａｕｎａｙ剖分的过程中,增加对三角形边界的判别、管理功能,记录其中作为点集凸包边界的线段,使得在实现剖分的同时产生出点集的凸包,从而提高了算法效率,且当该算法实现单一的点集剖分或凸包功能或是用于简单多边形的凸包与剖分时效果也很好     

空值环境下广义连接依赖（NGJD）及推导规则的研究

本文给出了空值环境下广义连接依赖强保持、弱保持的概念。讨论了它们的推导规则，证明了各推导规则在强保持、弱保持条件下的存在性，以及相应的完备性结论。     

分布式数据库下基于剪枝的并行合并连接策略

排序合并连接是数据库系统一种重要的连接实现方式,比哈希连接有更广泛的应用.分布式环境下,数据分片、分布存储,面对昂贵的网络代价,进行高效排序合并连接的挑战巨大.传统策略首先针对连接数据进行排序,然后基于排好序的数据执行合并连接.这两部分操作均基于原始数据进行操作,通常情况下,原始连接数据存在无用数据块,这些数据块无需连接,但会增加额外开销,包括网络开销.随着数据量的增多,出现无用数据块的概率增大,额外开销随之增多.传统策略没有预先处理这些无用数据块.针对这个问题,提出一种分布式环境下基于剪枝的并行排序合并连接策略（parallel sort-merge join based on prune,简称Pr_PSMJ）.其特点是,连接发生之前高效完成对连接对象无用数据块的剪枝处理,提高整体连接效率.基本思想是,根据连接对象对应的连接分区数据统计信息,构造一种双边邻接表（bilateral adjacency list,简称BAL）,用来对连接数据中无用数据块进行剪枝,并保证最终连接结果的正确性;剪枝完成后,利用BAL计算出各个最佳本地连接执行点,并指导分区数据的迁移,使数据移动量最小;在连接阶段,由于BAL保证本地连接执行节点的独立性,因此能够轻松并行执行整个连接过程,并在每个连接点本地利用多核环境完成局部并行排序合并连接;最后,将局部结果合并成最终结果.由于Pr_PSMJ中的高效剪枝策略是在连接执行之前完成的,因此几乎适合任何合并连接操作,并且对于其他连接策略也有借鉴作用.给出了基于Pr_PSMJ的算法的正确性、效率性以及适应性分析,并且给出实验验证,证明了在分布式大数据量排序合并连接情况下,Pr_PSMJ相对于其他策略能够有效减少网络开销,并提高连接效率.     

一种复杂多维层次的连接和聚集算法

由于数据仓库中存储着不同粒度、容量巨大的数据记录，所以如何有效地执行联机分析处理(OLAP)查询操作，特别是连接和聚集操作，便成为数据仓库领域的核心问题之一．为此，提出了一种降低连接和聚集操作的新算法(join and aggregation based on the complex multi-dimensional hierarchies，JACMDH)．算法充分考虑了复杂多维层次的特点，在原有的位图连接索引(bitmap join index)的基础上，采用层次联合代理(hierarchy combined surrogate)和预先分组排序的方法，使得复杂的多维层次上的连接和聚集操作转化成事实表上的区域查询，从而在处理多维层次聚集的同时，提高了连接和聚集的效率．算法性能分析和实验数据表明，JACMDH算法和目前流行的算法相比，其性能有显著的提高．     

空值环境下的NJD及其推导规则的研究

本文在空值环境下的ＮＦＤ，ＮＭＶＤ强，弱保持条件及相应的推导公理的基础上，讨论了空值环境下的连接依赖的强，弱保持成立的条件及相应定理。同时，讨论了ＮＪＤ在强，弱保持条件下的推导公理存在性问题。     

Structural Join and Staircase Join Algorithms of Sibling Relationship

The processing of XML queries can result in evaluation of various structural relationships. Efficient algorithms for evaluating ancestor-descendant and parent-child relationships have been proposed. Whereas the problems of evaluating preceding-sibling-following-sibling and preceding-following relationships are still open. In this paper, we studied the structural join and staircase join for sibling relationship. First, the idea of how to filter out and minimize unnecessary reads of elements using parent＇s structural information is introduced, which can be used to accelerate structural joins of parent-child and preceding-sibling-following-sibling relationships. Second, two efficient structural join algorithms of sibling relationship are proposed. These algorithms lead to optimal join performance： nodes that do not participate in the join can be judged beforehand and then skipped using B^＋-tree index. Besides, each element list joined is scanned sequentially once at most. Furthermore, output of join results is sorted in document order. We also discussed the staircase join algorithm for sibling axes. Studies show that, staircase join for sibling axes is close to the structural join for sibling axes and shares the same characteristic of high efficiency. Our experimental results not only demonstrate the effectiveness of our optimizing techniques for sibling axes, but also validate the efficiency of our algorithms. As far as we know, this is the first work addressing this problem specially.