一种基于消解的变量极小不可满足子公式的提取方法

变量极小不可满足(VMU)问题是极小不可满足(MU)问题的一个扩充和延伸.着重研究VMU子公式的提取算法.首先从理论上比较MU和VMU的基本性质,并分析了目前流行的MU子公式提取算法.研究Davis-Putman-消解的基本性质,给出一个判定变量极小不可满足公式的充分必要条件,进而提出一个基于消解的VMU子公式提取算法.此算法可以使用ZBDDs压缩存储消解式,并实现单步多重消解.     

一种基于抽象与精化技术的Web服务组合验证方法

模型检测因其自动化程度高、能够提供反例路径等优势,被广泛应用于Web服务组合的兼容性验证。本文针对模型检测过程中存在的状态爆炸问题,在传统的模型检测方法中引入谓词抽象和精化技术,提出了一种针对Web服务组合的抽象精化验证框架。使用谓词抽象技术对原子Web服务抽象建模,将各Web服务抽象模型组合成组合抽象模型;将模型检测后得到的反例在各原子Web服务上做投影操作,对投影反例进行确认;对产生伪反例的Web服务抽象模型进行精化,生成新的组合抽象模型,再次对性质进行验证。最后通过实例分析说明基于抽象精化技术的Web服务组合验证框架在缓解状态爆炸问题上的可行性。     

基于深度学习和反例制导的循环程序秩函数生成

程序终止性判定是程序分析与验证领域中的一个研究热点. 针对非线性循环程序, 提出了一种基于反例制导的神经网络型秩函数的构造方法. 该方法采用学习组件和验证组件交互的迭代框架, 其中学习组件利用程序轨迹作为训练集合构造一个候选秩函数, 验证组件运用可满足性模理论(Satisfiability Modulo Theories, SMT)确保候选秩函数的有效性, 而由SMT返回的反例则进一步用于扩展学习组件中的训练集合以对候选秩函数进行精化.实验结果表明, 所提出的方法比已有的机器学习方法在秩函数的构造效率和构造能力上具有优势.     

基于CEGAR的Web应用验证

Web应用导航行为的建模和验证是可信Web工程研究的重点和难点.在深入分析用户和Web浏览器交互行为的基础上,文中引入On-the-fly策略并基于反例引导的抽象精化验证方法 CEGAR对Web应用的导航行为进行建模和验证.在On-the-fly导航模型展开的过程中,根据检验性质采用增量式状态抽象方法构造Web应用导航抽象模型,通过确认抽象反例来识别伪反例,借助等价类精化方法消除抽象模型上的伪反例.这一方法可有效地缓解Web应用验证过程中出现的状态爆炸问题.     

构件组合的抽象精化验证

针对构件组合的状态爆炸问题,改进了反例引导的抽象精化框架,提出了组合式的抽象精化方法,使构件组合的模型检验转化为各成分构件的局部抽象精化,降低了分析的复杂度.提出了在构件组合情况下基于等价关系和存在商的构件抽象方法,用构件抽象的组合建立构件组合的抽象;提出了组合确认定理并给出证明,使反例确认分解为在各构件上对反例投影的确认;通过对单个构件的等价关系的精化实现构件组合的抽象模型的精化.在模型检验构件组合的过程中,不需要为构件组合建立全局的具体状态空间.     

面向未解释程序的合作验证方法

未解释程序的验证问题通常是不可判定的,但是最近有研究发现,存在一类满足coherence性质的未解释程序,其验证问题是可判定的,并且计算复杂度为PSPACE完全的.在这个结果的基础上,一个针对一般未解释程序验证的基于路径抽象的反例抽象精化（CEGAR）框架被提出,并展现了良好的验证效率.即使如此,对未解释程序的验证工作依然需要多次迭代,特别是利用该方法在针对多个程序验证时,不同的程序之间的验证过程是彼此独立的,存在验证开销巨大的问题.本文发现被验证的程序之间较为相似时,不可行路径的抽象模型可以在不同的程序之间复用.因此,本文提出了一个合作验证的框架,收集在验证过程中不可行路径的抽象模型,并在对新程序进行验证时,用已保存的抽象模型对程序进行精化,提前删减一些已验证的程序路径,从而提高验证效率.此外,本文通过对验证过程中的状态信息进行精简,对现有的基于状态等价的路径抽象方法进行优化,以进一步提升其泛化能力.本文对合作验证的框架以及路径抽象的优化方法进行了实现,并在两个具有代表性的程序集上分别取得了2.70x和1.49x的加速.     

基于广义符号轨迹赋值模型验证的反例的产生

广义符号轨迹赋值(Symbolic Trajectory Evaluation)引入了符号变量和抽象技术,解决了验证中状态爆炸的问题,但是却为寻找反例制造了很多障碍.针对此,提出了一种高效的寻找反例的算法,它应用集合的概念,通过回溯在父子路径之间进行集合的交集,可以高效地解决抽象引起的问题.并对此算法进行改进,解决了符号变量带来的问题.     

基于悖论分析和增量求解的快速反例压缩算法

使用反例压缩算法,从反例中剔除冗余信息,从而使反例易于理解,是目前的研究热点.然而,目前压缩率最高的BFL(brute force lifting)算法,其时间开销过大.为此,提出一种基于悖论分析和增量式SAT(boolean satisfiablilty problem)的快速反例压缩算法.首先,根据反证法和排中律原理,该算法对每一个自由变量v,构造一个SAT问题,以测试v是否能够避免反例.而后对其中不可满足的SAT问题,进行悖论分析,抽取出导致悖论的变量集合.所有不属于该集合的变量,均可作为无关变量直接剔除.同时,该算法使用增量式SAT求解方法,以避免反复搜索冗余状态空间.理论分析和实验结果表明,与BFL算法相比,该算法能够在不损失压缩率的前提下获得1～2个数量级的加速.     

反例引导的模型检验工具的设计

针对模型组合中常见的"状态空间爆炸"问题,分析了抽象和组合两种方法各自的优缺点,采用"反例引导的抽象精化"框架和模型检验思想,将抽象和组合结合起来,为模型组合的检验提出了一种新的方法.设计了模型的抽象、组合、检验和精化算法,开发了一款基于反例引导的、图形化的模型检验工具,使用Kripke结构建立模型,用LTL描述性质,从而表明了反例引导的模型检验方法的过程.     

一种C程序断言的全自动静态验证方法

在软件程序中插入断言是保证软件质量的一个简单但有效的方法，人们常使用测试的方法检验程序中的断言是否满足，但测试很难保证验证的完备性。本文提出了一种可以保证完备性的全自动静态断言验证方法，其基本思想是基于程序切片符号执行程序的所有执行路径，并证明路径上的所有断言都满足。为了尽量减少符号执行的语句的数量，使用了基于反例的抽象精化方法，从一个粗略的切片标准开始迭代地符号执行一爷路径，根据验证的反例自动生成下一次迭代过程中使用的精化的切片标准。包含循环的程序可能具有无穷多条程序执行路径，提出的基于符号执行上下文不变式证明的方法可以证明由于循环导致的无穷多条路径中断言都满足，从而使得验证过程可以终止。实验表明，提出的全自动静态断言验证方法不仅可行，而且验证代价较小，具有较强的实用性。     

An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF

We consider the minimal unsatisfiability problem for propositional formulas over n variables with n+k clauses for fixedk. We will show that in case of at most n clauses no formula is minimal unsatisfiable. For n+1 clauses the minimal unsatisfiability problem is solvable in quadratic time. Further, we present a characterization of minimal unsatisfiable formulas with n+1clauses in terms of a certain form of matrices. This revised version was published online in June 2006 with corrections to the Cover Date.     

Cost analysis of the longest-side (triangle bisection) refinement algorithm for triangulations

The triangulation refinement problem, as formulated in the adaptive finite element setting (also useful in the rendering of complex scenes), is discussed. This can be formulated as follows: given a valid, non-degenerate triangulation of a polygonal region, construct a locally refined triangulation, with triangles of prescribed size in a refinement regionR, and such that the smallest (or the largest) angle is bounded. To cope with this problem, longest-side refinement algorithms guarantee the construction of good quality irregular triangulations. This is due in part to their natural refinement propagation strategy farther than the (refinement) area of interestR. In this paper we prove that, asymptotically, the numberN of points inserted inR to obtain triangles of prescribed size, is optimal. Furthermore, in spite of the unavoidable propagation outside the refinement regionR, the time cost of the algorithm is linear inN, independent of the size of the triangulation. Specifically, the number of points inserted outsideR is of orderO(n log ₂ n) whereN=O(n²). We prove the latter result for circular and rectangular refinement regions, which allows us to conclude that this is true for general convex refinement regions. We also include empirical evidence, both in two and three dimensions, which is in complete agreement with the theory, even for small values ofN.     

Proving refinement using transduction

Summary. When designing distributed systems, one is faced with the problem of verifying a refinement between two specifications, given at different levels of abstraction. Suggested verification techniques in the literature include refinement mappings and various forms of simulation. We present a verification method, in which refinement between two systems is proven by constructing a transducer that inputs a computation of a concrete system and outputs a matching computation of the abstract system. The transducer uses a FIFO queue that holds segments of the concrete computation that have not been matched yet. This allows a finite delay between the occurrence of a concrete event and the determination of the corresponding abstract event. This delay often makes the use of prophecy variables or backward simulation unnecessary. An important generalization of the method is to prove refinement modulo some transformation on the observed sequences of events. The method is adapted by replacing the FIFO queue by a component that allows the appropriate transformation on sequences of events. A particular case is partial-order refinement, i.e., refinement that preserves only a subset of the orderings between events of a system. Examples are sequential consistency and serializability. The case of sequential consistency is illustrated on a proof of sequential consistency of a cache protocol.     

不可满足公式的同态证明系统

合取范式(CNF)公式H到F的同态φ是一个从H的文字集合到F的文字集合的映射,并保持补运算和子句映到子句.同态映射保持一个公式的不可满足性.一个公式是极小不可满足的是指该公式本身不可满足,而且从中删去任意一个子句后得到的公式可满足.MU(1)是子句数与变元数的差等于1的极小不可满足公式类.一个三元组(H,φ,F)称为的一个来自H的同态证明,如果φ是一个从H到F的同态.利用基础矩阵的方法证明了:一个不可满足公式F的树消解证明,可以在多项式时间内转换成一个来自MU(1)中公式的同态证明.从而,由MU(1)中的公式构成的同态证明系统是完备的,并且由MU(1)中的公式构成的同态证明系统与树消解证明系统之间是多项式等价的.     

On the weakest failure detector ever

Many problems in distributed computing are impossible to solve when no information about process failures is available. It is common to ask what information about failures is necessary and sufficient to circumvent some specific impossibility, e.g., consensus, atomic commit, mutual exclusion, etc. This paper asks what information about failures is necessary to circumvent any impossibility and sufficient to circumvent some impossibility. In other words, what is the minimal yet non-trivial failure information. We present an abstraction, denoted U{\Upsilon} , that provides very little information about failures. In every run of the distributed system, U{\Upsilon} eventually informs the processes that some set of processes in the system cannot be the set of correct processes in that run. Although seemingly weak, for it might provide random information for an arbitrarily long period of time, and it eventually excludes only one set of processes (among many) that is not the set of correct processes in the current run, U{\Upsilon} still captures non-trivial failure information. We show that U{\Upsilon} is sufficient to circumvent the fundamental wait-free set-agreement impossibility. While doing so, (a) we disprove previous conjectures about the weakest failure detector to solve set-agreement and (b) we prove that solving set-agreement with registers is strictly weaker than solving n + 1-process consensus using n-process consensus. We show that U{\Upsilon} is the weakest stable non-trivial failure detector: any stable failure detector that circumvents some wait-free impossibility provides at least as much information about failures as U{\Upsilon} does. Our results are generalized, from the wait-free to the f-resilient case, through an abstraction U^f{\Upsilon^f} that we introduce and prove minimal to solve any problem that cannot be solved in an f-resilient manner, and yet sufficient to solve f-resilient f-set-agreement.     

Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. However, the state-space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. Even in the case of purely sequential programs, a crucial requirement to make predicate abstraction effective is to use as few predicates as possible. This is because, in the worst case, the state-space of the abstraction generated (and consequently the time and memory complexity of the abstraction process) is exponential in the number of predicates involved. In addition, for concurrent programs, the number of reachable states could grow exponentially with the number of components. We attempt to address these issues in the context of verifying concurrent (message-passing) C programs against safety specifications. More specifically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (predicate abstraction for data and action-guided abstraction for events) within a counterexample-guided abstraction refinement scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specification is either established or refuted. Additionally, a key feature of our approach is that if a property can be proved to hold or not hold based on a given finite set of predicates $\mathcal{P}$ , the predicate refinement procedure we propose in this article finds automatically a minimal subset of $\mathcal{P}$ that is sufficient for the proof. This, along with our explicit use of compositionality, delays the onset of state-space explosion for as long as possible. We describe our approach in detail, and report on some very encouraging experimental results obtained with our tool MAGIC.     

Encoding, Decoding and Data Refinement

Data refinement is the systematic replacement of a data structure with another one in program development. Data refinement between program statements can on an abstract level be described as a commutativity property where the abstraction relationship between the data structures involved is represented by an abstract statement (a decoding). We generalise the traditional notion of data refinement by defining an encoding operator that describes the least (most abstract) data refinement with respect to a given abstraction. We investigate the categorical and algebraic properties of encoding and describe a number of special cases, which include traditional notions of data refinement. The dual operator of encoding is decoding, which we investigate and give an intuitive interpretation to. Finally we show a number of applications of encoding and decoding. Received May 1999 / Accepted in revised form November 2000     

Extended version with the analysis of dynamic system for iterative refinement of solution

The extended version with the analysis of dynamic system for Wilkinson's iteration improvement of solution is presented in this paper. It turns out that the iteration improvement can be viewed as applying explicit Euler method with step size h=1 to a dynamic system which has a unique globally asymptotically stable equilibrium point, that is, the solution x*=A ^?1 b of linear system Ax=b with non-singular matrix A. As a result, an extended iterative improvement process for solving ill-conditioned linear system of algebraic equations with non-singular coefficients matrix is proposed by following the solution curve of a linear system of ordinary differential equations. We prove the unconditional convergence and derive the roundoff results for the extended iterative refinement process. Several numerical experiments are given to show the effectiveness and competition of the extended iteration refinement in comparison with Wilkinson's.     

Fixed-Parameter Enumerability of Cluster Editing and Related Problems

Cluster Editing is transforming a graph by at most k edge insertions or deletions into a disjoint union of cliques. This problem is fixed-parameter tractable (FPT). Here we compute concise enumerations of all minimal solutions in O(2.27 ^k +k ² n+m) time. Such enumerations support efficient inference procedures, but also the optimization of further objectives such as minimizing the number of clusters. In an extended problem version, target graphs may have a limited number of overlaps of cliques, measured by the number t of edges that remain when the twin vertices are merged. This problem is still in FPT, with respect to the combined parameter k and t. The result is based on a property of twin-free graphs. We also give FPT results for problem versions avoiding certain artificial clusterings. Furthermore, we prove that all solutions with minimal edit sequences differ on a so-called full kernel with at most k ²/4+O(k) vertices, that can be found in polynomial time. The size bound is tight. We also get a bound for the number of edges in the full kernel, which is optimal up to a (large) constant factor. Numerous open problems are mentioned.