基于不变式生成的循环停机性验证

循环的停机性验证是程序验证中的一个难点。程序不变式用来描述程序变量的取值关系,其中线性不变式可以帮助描述程序变量间的线性关系,循环不变式能够有效刻画循环中的变量关系。本文基于线性不变式和多项式循环不变式的生成,将循环的停机性验证转化为求解一个最优化问题,给出了一个实用的程序停机性验证框架。基于该框架可以自动地验证程序的停机性,并给出循环的复杂度上界。实验结果说明了该方法的实用性。     

基于执行序列的程序时间复杂度分析

为了达到更准确、更高效的程序时间复杂度,解决复杂度分析中的循环下的复杂情况,如多个跳出点、嵌套循环和非数值域循环等,提出了基于执行序列计算复杂度的方法。提取出程序方法的各条可能的执行序列及其各条执行序列的相关约束条件和执行效应,在此基础上分析出序列间的关系从而计算出最终的时间复杂度。基于这种方法开发出的工具,通过几个大型的实际程序,发现这种方法可以有效地计算出其中大于90%的方法的运行复杂度。     

周期为2n的二元序列k错2-adic复杂度算法

首先设计了一个计算周期为2^n的二元序列的2-adic复杂度综合算法．随后,以该算法为基础,给出了一个计算周期为2^n的二元序列的k错2-adic复杂度综合算法．使用这两个算法可以分别在n步内计算得到序列的2-adic复杂度上界以及k错2-adic复杂度上界．     

基于抽象解释理论的循环边界计算方法

在实时系统的应用中常常需要对系统的执行时间,尤其是最坏执行时间进行分析。而程序中的循环结构的迭代次数对程序执行时间的分析结果具有重要的影响。程序的循环边界分析目的在于给出较为接近程序真实运行情况下的循环结构迭代的上界和下界。提出了一种基于抽象解释理论的程序循环边界计算方法,该方法对原有的循环边界分析方法进行了改进。首先在程序切片阶段对原程序建立程序依赖图,并提出了对程序依赖图的约简方法。由约简后的依赖关系可以对变量的取值进行约束,得到更小的取值范围,因此基于该方法的循环边界分析结果更加接近程序的实际执行边界,对获取精确的程序执行时间具有重要意义。     

大规模核方法的随机假设空间方法

大规模核方法是大规模数据分析与挖掘的基本机器学习方法。核方法在再生核希尔伯特空间中训练线性学习器求解样本空间中的非线性问题,求解时间复杂度关于数据规模是平方级的,预测也依赖于整个训练数据,因而不适用于大规模学习问题。针对这些问题,提出了大规模核方法的有效随机假设空间方法。首先,在关于样本维度对数时间复杂度内,应用循环随机特征映射显式构造假设空间,该空间称之为循环随机假设空间。然后,在循环随机假设空间中应用线性或亚线性学习算法训练线性模型。理论上,给出了循环随机假设空间的一致泛化误差上界及其相对于最优泛化误差的收敛性。实验结果表明,大规模核方法的随机假设空间方法不仅能够显著地提高非线性核方法的训练与预测效率,而且能够保持与非线性核方法相当的预测精度。该方法有理论保障,计算复杂度低,运行效率高,是当前最高效的大规模核方法实现方法。     

单分支线性约束循环程序的终止性分析

秩函数法是循环终止性分析的主要方法,秩函数的存在表明了循环程序是可终止的.针对单分支线性约束循环程序,提出一种方法对此类循环的终止性进行分析.基于增函数法向空间的计算,该方法将原程序空间上的秩函数计算问题归结为其子空间上的秩函数计算问题.实验结果表明,该方法能有效验证现有文献中大部分循环程序的终止性.     

分形理论在软件复杂度中的应用

利用分形理论对软件复杂度进行研究,给出盒子及程序分形复杂度的定义,进一步给出了算法思想和计算方法,并通过实例说明程序具有分形特征——标度不变性。在此基础上,对一些程序的分形复杂度进行了计算,并通过进一步的分析表明所得数值在某种情况下可以反映出程序在结构上的复杂程度,其度量结果是比较有效的。     

使用符号化形式语言MATHEMTICATM~TM进行机器人操作器的计算

本文提供了一个用符号化形式语言计算机器人操作器的程序,所使用的符号化形式语言为Mathematic~(TM),本程序可以用来解机器人操作器的运动学方程式及建立拉格朗日动力学方程式,等等。并用两个实例示范如何使用本程序建立运动学方程式及计算斯坦福操作器。     

时滞项可微系统的时滞依赖的稳定性条件

本文研究了带有可微时滞项连续系统的稳定性问题. 通过利用时滞项导数的信息, 给出了改进的时滞系统渐近稳定性条件. 与已有的做法不同, 即便是时滞项导数的上界大于等于 1 时这个上界仍可被利用. 文中证明了所得结果比已有结果的保守性小. 同时, 由于涉及较少的决策变量, 计算复杂度也大为降低. 数例进一步说明了所得结果的有效性和少保守性.     

Fibonacci数和Lucas数的联合迭代算法

针对超大Fibonacci数和Lucas数的计算问题,提出一种Fibonacci-Lucas数联合迭代算法,在单次循环中选择二倍步长的方式,采用交替计算Fibonacci数和Lucas数的方法,减低超大数迭代算式的复杂度,提高程序的计算效率。实验结果表明,该算法运行时间比现有的矩阵迭代算法更短。     

Lower Bounds for Runtime Complexity of Term Rewriting

We present the first approach to deduce lower bounds for (worst-case) runtime complexity of term rewrite systems (TRSs) automatically. Inferring lower runtime bounds is useful to detect bugs and to complement existing methods that compute upper complexity bounds. Our approach is based on two techniques: the induction technique generates suitable families of rewrite sequences and uses induction proofs to find a relation between the length of a rewrite sequence and the size of the first term in the sequence. The loop detection technique searches for “decreasing loops”. Decreasing loops generalize the notion of loops for TRSs, and allow us to detect families of rewrite sequences with linear, exponential, or infinite length. We implemented our approach in the tool AProVE and evaluated it by extensive experiments.     

A cost-effective implementation of multilevel tiling

This paper presents a new cost-effective algorithm to compute exact loop bounds when multilevel tiling is applied to a loop nest having affine functions as bounds (nonrectangular loop nest). Traditionally, exact loop bounds computation has not been performed because its complexity is doubly exponential on the number of loops in the multilevel tiled code and, therefore, for certain classes of loops (i.e., nonrectangular loop nests), can be extremely time consuming. Although computation of exact loop bounds is not very important when tiling only for cache levels, it is critical when tiling includes the register level. This paper presents an efficient implementation of multilevel tiling that computes exact loop bounds and has a much lower complexity than conventional techniques. To achieve this lower complexity, our technique deals simultaneously with all levels to be tiled, rather than applying tiling level by level as is usually done. For loop nests having very simple affine functions as bounds, results show that our method is between 15 and 28 times faster than conventional techniques. For loop nests caving not so simple bounds, we have measured speedups as high as 2,300. Additionally, our technique allows eliminating redundant bounds efficiently. Results show that eliminating redundant bounds in our method is between 22 and 11 times faster than in conventional techniques for typical linear algebra programs.     

Using Vapnik–Chervonenkis Dimension to Analyze the Testing Complexity of Program Segments

We examine the complexity of testing different program constructs. We do this by defining a measure of testing complexity known as VCP-dimension, which is similar to the Vapnik–Chervonenkis dimension, and applying it to classes of programs, where all programs in a class share the same syntactic structure. VCP-dimension gives bounds on the number of test points needed to determine that a program is approximately correct, so by studying it for a class of programs we gain insight into the difficulty of testing the program construct represented by the class. We investigate the VCP-dimension of straight line code, if–then–else statements, and for loops. We also compare the VCP-dimension of nested and sequential if–then–else statements as well as that of two types of for loops with embedded if–then–else statements. Finally, we perform an empirical study to estimate the expected complexity of straight line code.     

Probability intervals over influence diagrams

A mechanism for performing probabilistic reasoning in influence diagrams using interval rather than point-valued probabilities is described. Procedures for operations corresponding to conditional expectation and Bayesian conditioning in influence diagrams are derived where lower bounds on probabilities are stored at each node. The resulting bounds for the transformed diagram are shown to be the tightest possible within the class of constraints on probability distributions that can be expressed exclusively as lower bounds on the component probabilities of the diagram. Sequences of these operations can be performed to answer probabilistic queries with indeterminacies in the input and for performing sensitivity analysis on an influence diagram. The storage requirements and computational complexity of this approach are comparable to those for point-valued probabilistic inference mechanisms     

Loop coalescing and scheduling for barrier MIMD architectures

Barrier MIMD's are asynchronous multiple instruction stream, multiple data stream architectures capable of parallel execution of variable execution time instructions and arbitrary control flow (e.g., while loops and calls); however, they differ from conventional MIMD's in that the need for run-time synchronization is significantly reduced. The authors consider the problem of scheduling nested loop structures on a barrier MIMD. The basic approach employs loop coalescing, a technique for transforming a multiply-nested loop into a single loop. Loop coalescing is extended to nested triangular loops, in which inner loop bounds are functions of outer loop indices. In addition, a more efficient scheme to generate the original loop indices from the coalesced index is proposed for the case of constant loop bounds. These results are general, and can be applied to extend previous work using loop coalescing techniques. The authors concentrate on using loop coalescing for scheduling barrier MIMDs, and show how previous work in loop transformations and linear scheduling theory can be applied to this problem     

A knowledge-based approach to the analysis of loops

The paper presents a knowledge-based analysis approach that generates first order predicate logic annotations of loops. A classification of loops according to their complexity levels is presented. Based on this taxonomy, variations on the basic analysis approach that best fit each of the different classes are described. In general, mechanical annotation of loops is performed by first decomposing them using data flow analysis. This decomposition encapsulates closely related statements in events, that can be analyzed individually. Specifications of the resulting loop events are then obtained by utilizing patterns, called plans, stored in a knowledge base. Finally, a consistent and rigorous functional abstraction of the whole loop is synthesized from the specifications of its individual events. To test the analysis techniques and to assess their effectiveness, a case study was performed on an existing program of reasonable size. Results concerning the analyzed loops and the plans designed for them are given     

Decision procedures for inductive Boolean functions based on alternating automata

We show how alternating automata provide decision procedures for the equality of inductively defined Boolean functions and present applications to reasoning about parameterized families of circuits. We use alternating word automata to formalize families of linearly structured circuits and alternating tree automata to formalize families of tree structured circuits. We provide complexity bounds for deciding the equality of function (or circuit) families and show how our decision procedures can be implemented using BDDs. In comparison to previous work, our approach is simpler, has better complexity bounds, and, in the case of tree-structured families, is more general.     

An efficient code generation technique for tiled iteration spaces

This paper presents a novel approach for the problem of generating tiled code for nested for-loops, transformed by a tiling transformation. Tiling or supernode transformation has been widely used to improve locality in multilevel memory hierarchies, as well as to efficiently execute loops onto parallel architectures. However, automatic code generation for tiled loops can be a very complex compiler work, especially when nonrectangular tile shapes and iteration space bounds are concerned. Our method considerably enhances previous work on rewriting tiled loops, by considering parallelepiped tiles and arbitrary iteration space shapes. In order to generate tiled code, we first enumerate all tiles containing points within the iteration space and, second, sweep all points within each tile. For the first subproblem, we refine upon previous results concerning the computation of new loop bounds of an iteration space that has been transformed by a nonunimodular transformation. For the second subproblem, we transform the initial parallelepiped tile into a rectangular one, in order to generate efficient code with the aid of a nonunimodular transformation matrix and its Hermite Normal Form (HNF). Experimental results show that the proposed method significantly accelerates the compilation process and generates much more efficient code.     

Container of (min, +)-linear systems

Based on the (min,+)-linear system theory, the work developed here takes the set membership approach as a starting point in order to obtain a container for ultimately pseudo-periodic functions representative of Discrete Event Dynamic Systems. Such a container, by approximating the exact system, ensures to entirely include it in a guaranteed way. To reach that point, the container introduced in this paper is given as an interval, the bounds of which are a convex function for the upper approximation and a concave function for the lower approximation. Thanks to the characteristics of the bounds, the aim is both to reduce data storage (that can be very high when exact functions are handled) and to reduce the algorithm complexity of the operations of sum, inf-convolution and subadditive closure. These operations are integrated into inclusion functions, the algorithms of which are of linear or quasi-linear complexity.