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

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

共形几何代数与几何不变量的代数运算

几何不变量的使用是计算机视觉和图形学的一个重要手段.发现一个不变量后,如何找到它与其他不变量的关系,是实际应用中的一个重要问题,这种关系的探讨主要依靠在不变量层次上的代数运算.文中介绍了共形几何代数中的基本、高级和有理不变量如何在几何问题中自然出现,它们之间如何进行代数运算,以及如何通过不变量的化简,自然地得到几何条件的充分必要化和几何定理的完全化.几何定理的机器证明作为几何定理完全化的副产品,被发展成几何定理的关系定量化,这种量化的几何还原就是几何定理的自然推广.几何不变量之间的几何关系的计算是这些技术的一个具体应用.     

Proof planning for strategy development

Proof planning extends the tactic-based theorem proving paradigm through the explicit representation of proof strategies. We see three key benefits to the proof planning approach to the development of proof strategies: flexibility, re-usability and synergy. Here we demonstrate these benefits in terms of reasoning about imperative programs where we reuse strategies developed previously for proof by mathematical induction. In particular, we focus upon strategies for automating the discovery of loop invariants. Our approach tightly couples the discovery of invariants with the process of patching proof strategy failures. This revised version was published online in June 2006 with corrections to the Cover Date.     

Case studies of Z-module reasoning: Proving benchmark theorems from ring theory

A new method, called Z-module reasoning, was formulated for proving and discovering theorems from ring theory. In a case study, the ZMR system designed to implement this method was used to prove the benchmark x ³ ring theorem from associative ring theory. The system proved the theorem quite efficiently. The system was then used to prove the x ⁴ ring theorem from associative ring theory. Again, a proof was produced easily. These proofs, together with the successes in proving other difficult theorems from ring theory suggest that the Z-module reasoning method is useful for solving a class of problems relying on equality reasoning. This paper illustrates the Z-module reasoning method, and analyzes the computer proof of the x ³ ring theorem.This reasearch was supported in part by the Applied Mathematical Sciences subprogram of the office of Energy Research, U.S. Department of Energy, under contract W-31-109-Eng-38.     

Loop summarization using state and transition invariants

This paper presents algorithms for program abstraction based on the principle of loop summarization, which, unlike traditional program approximation approaches (e.g., abstract interpretation), does not employ iterative fixpoint computation, but instead computes symbolic abstract transformers with respect to a set of abstract domains. This allows for an effective exploitation of problem-specific abstract domains for summarization and, as a consequence, the precision of an abstract model may be tailored to specific verification needs. Furthermore, we extend the concept of loop summarization to incorporate relational abstract domains to enable the discovery of transition invariants, which are subsequently used to prove termination of programs. Well-foundedness of the discovered transition invariants is ensured either by a separate decision procedure call or by using abstract domains that are well-founded by construction. We experimentally evaluate several abstract domains related to memory operations to detect buffer overflow problems. Also, our light-weight termination analysis is demonstrated to be effective on a wide range of benchmarks, including OS device drivers.     

An integral theorem prover and the role of proof planning

An investigation is made into the ways proof planning can enhance the capability of a rule based prover for the theory of integration. The integrals are of the Riemann type and are defined in a way to maximize the theorem proving methods of predicate calculus. Approximately fifty theorems have been proved and several examples are discussed. A major shortcoming was found to be the inability of the system to work with or produce a proof plan. As a result, a planning scheme based on the idea of subgoals or milestones was considered. With user defined plans, there was a substantial increase in performance and capability of the system and, in some cases, proofs which were previously unsuccessful were completed.     

Automatic Generation of Invariants

When proving invariance properties of programs, one is faced with two problems. The first problem is related to the necessity of proving tautologies of the considered assertion language, whereas the second manifests itself in the need of finding sufficiently strong invariants. This paper focuses on the second problem and describes techniques for the automatic generation of invariants. The first set of these techniques is applicable to sequential transition systems and allows deriving so-called local invariants, i.e., predicates which are invariant at some control location. The second is applicable on networks of transition systems and allows combining local invariants of the sequential components to obtain local invariants of the global system.     

Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods

We present a symbolic-numeric hybrid method, based on sum-of-squares (SOS) relaxation and rational vector recovery, to compute inequality invariants and ranking functions for proving total correctness and generating preconditions for programs. The SOS relaxation method is used to compute approximate invariants and approximate ranking functions with floating point coefficients. Then Gauss-Newton refinement and rational vector recovery are applied to approximate polynomials to obtain candidate polynomials with rational coefficients, which exactly satisfy the conditions of invariants and ranking functions. In the end, several examples are given to show the effectiveness of our method.     

Invariant based programming: basic approach and teaching experiences

Program verification is usually done by adding specifications and invariants to the program and then proving that the verification conditions are all true. This makes program verification an alternative to or a complement to testing. We describe here another approach to program construction, which we refer to as invariant based programming, where we start by formulating the specifications and the internal loop invariants for the program, before we write the program code itself. The correctness of the code is then easy to check at the same time as one is constructing it. In this approach, program verification becomes a complement to coding rather than to testing. The purpose is to produce programs and software that are correct by construction. We present a new kind of diagrams, nested invariant diagrams, where program specifications and invariants (rather than the control) provide the main organizing structure. Nesting of invariants provide an extension hierarchy that allows us to express the invariants in a very compact manner. We have studied the feasibility of formulating specifications and loop invariants before the code itself has been written in a number of case studies. Our experience is that a systematic use of figures, in combination with a rough idea of the intended behavior of the algorithm, makes it rather straightforward to formulate the invariants needed for the program, to construct the code around these invariants and to check that the resulting program is indeed correct. We describe our experiences from using invariant based programming in practice, both from teaching programmers how to construct programs that they prove correct themselves, and from teaching invariant based programming for CS students in class. D. A. Duce, J. Oliveira, P. Boca and R. Boute     

Uniform strategies: The CADE-11 theorem proving contest

At CADE-10 Ross Overbeek proposed a two-part contest to stimulate and reward work in automated theorem proving. The first part consists of seven theorems to be proved with resolution, and the second part of equational theorems. Our theorem proversOtter and its parallel childRoo proved all of the resolution theorems and half of the equational theorems. This paper represents a family of entries in the contest.     

Automated theorem proving in mathematics

TheMuscadet theorem prover is a knowledge-based system able to prove theorems in some non-trivial mathematical domains. The knowledge bases contain some general deduction strategies based onnatural deduction, mathematical knowledge and metaknowledge. Metarules build new rules, easily usable by the inference engine, from formal definitions. Mathematical knowledge may be general or specific to some particular field.Muscadet proved many theorems in set theory, mappings, relations, topology, geometry, and topological linear spaces. Some of the theorems were rather difficult.Muscadet is now intended to become an assistant for mathematicians in discrete geometry for cellular automata. In order to evaluate the difficulty of such a work, researchers were observed while proving some lemmas, andMuscadet was tested on easy ones. New methods have to be added to the knowledge base, such as reasoning by induction, but also new heuristics for splitting and reasoning by cases. It is also necessary to find good representations for some mathematical objects.     

A pragmatic approach to resolution-based theorem proving

Resolution theory offers a simple, complete method for proving theorems but is generally considered impractical. The theorems we are interested in proving arise in the analysis of programs and usually involve quantification. We have developed a system for proving these theorems using resolution, but have embedded in it a simplifier as the central component. The simplifier is an integrated collection of algorithms for normalizing arithmetic, relational, and logical expressions. The knowledge in the simplifier is encoded in procedures, rather than as axioms or rules. We use the simplifier to prove certain theorems, reduce the clutter in theorems, and reduce the cost of unification, Inherent in the normal form algorithms is the notion of strengthening (e.g., inferringa =b froma b ANDb a). We have incorporated the notion into the unification algorithm as well. The design of the system permits its use along a spectrum from pure resolution to resolution with interpretation of the arithmetic and relational operators. Strengthening is a heuristic that permits the movement along this spectrum. We call the approachi-resolution.i-resolution does not preserve completeness; it does define a means for approaching completeness efficiently and systematically. It thus attempts to provide a pragmatic approach to mechanical theorem proving.     

Improved Invariant Generation for Tvoc

The NYU Tvoc project applies the method of translation validation to verify that optimized code is semantically equivalent to the unoptimized code, by establishing, for each run of the optimizing compiler, a set of verification conditions (VCs) whose validity implies the correctness of the optimized run. The core of Tvoc is Tvoc-sp, that handles structure preserving optimizations, i.e., optimizations that do not alter the inner loop structures. The underlying proof rule, Val, on whose soundness Tvoc-sp is based, requires, among other things, to generating invariants at each “cutpoint” of the control graph of both source and target codes. The current implementation of Tvoc-sp employs somewhat naïve fix-point computations to obtain the invariants. In this paper, we propose an alternative method to compute invartiants which is based on simple data-flow analysis techniques.     

Isotopic meshing of implicit surfaces

Implicit surfaces are given as the zero set of a function F:ℝ³→ℝ. Although several algorithms exist for generating piecewise linear approximations, most of these are based on a user-defined stepsize or bounds to indicate the precision, and therefore cannot guarantee topological correctness. Interval arithmetic provides a mechanism to determine global properties of the implicit function. In this paper we present an algorithm that uses these properties to generate a piecewise linear approximation of implicit curves and surfaces, that is isotopic to the curve or surface itself. The algorithm is simple and fast, and is among the first to guarantee isotopy for implicit surface meshing.     

Basic principles of mechanical theorem proving in elementary geometries

At the end of 1976 and the beginning of 1977, the author discovered a mechanical method for proving theorems in elementary geometries. This method can be applied to various unordered elementary geometries satisfying the Pascalian Axiom, or to theorems not involving the concept of ‘order’ (e.g., thatc is ‘between’a andb) in various elementary geometries. In Section 4 we give the detailed proofs of the basic principles underlying this method. In Sections 2 and 3 we present the theory of well-ordering of polynomials and a constructive theory of algebraic varieties. Our method is based on these theories, both of which are based on the work of J. F. Ritt. In Section 5 we use Morley's theorem and the Pascal-conic theorem discovered by the author to illustrate the computer implementation of the method.     

Component-based verification using incremental design and invariants

We propose invariant-based techniques for the efficient verification of safety and deadlock-freedom properties of component-based systems. Components and their interactions are described in the BIP language. Global invariants of composite components are obtained by combining local invariants of their constituent components with interaction invariants that take interactions into account. We study new techniques for computing interaction invariants. Some of these techniques are incremental, i.e., interaction invariants of a composite hierarchically structured component are computed by reusing invariants of its constituents. We formalize incremental construction of components in the BIP language as the process of building progressively complex components by adding interactions (synchronization constraints) to atomic components. We provide sufficient conditions ensuring preservation of invariants when new interactions are added. When these conditions are not satisfied, we propose methods for generating new invariants in an incremental manner by reusing existing invariants from the constituents in the incremental construction. The reuse of existing invariants reduces considerably the overall verification effort. The techniques have been implemented in the D-Finder toolset. Among the experiments conducted, we have been capable of verifying safety properties and deadlock-freedom of sub-systems of the functional level of the DALA autonomous robot. This work goes far beyond the capacity of existing monolithic verification tools.     

Improving the time efficiency of proving theorems using a learning mechanism

In this paper, we develop a new approach for enhancing the time efficiency of proving theorems by using a learning mechanism. A system is proposed for analyzing a set of theorems and observing those features that often affect the speed at which the theorems are proved. The system uses the learning mechanism for choosing between two well known theorem-provers, namely, Resolution–Refutation (TGTP) and Semantic Trees (HERBY). A three-step process has been implemented. The first step is to prove a set of theorems using the above two theorem provers. A training set of two classes of theorems is thus created. Each class represents those theorems that have been proven in less time using a particular theorem prover. The second step is to train neural networks on both classes of theorems in order to construct an internal representation of the decision boundary between the two classes. In the last step, a voting scheme is invoked in order to combine the decisions of the individual neural networks into a final decision. The results achieved by the system when working on the standard theorems of the Stickel Test Set are shown. Those results confirm the feasibility of our approach to inte-grate a learning mechanism into the process of automated theorem proving.     

Extended two-dimensional DTM and its application on nonlinear PDEs with proportional delay

In this work, we successfully extended two-dimensional differential transform method and their reduced form, by presenting and proving some theorems, to obtain the solution of partial differential equations (PDEs) with proportional delay in t and shrinking in x. Theorems are presented in the most general form to cover a wide range of PDEs, being linear or nonlinear and constant or variable coefficient. In order to show the power and robustness of the present methods and to illustrate the pertinent features of related theorems, some examples are presented.     

Straightening Euclidean invariants

The Gröbner basis method is a powerful tool in automated geometry theorem proving. Normally, one works in the ring of coordinates of the points in a particular configuration. Tim Havel has suggested using instead the ring of interpoint squared distances because it is the invariant subring under the group of Euclidean isometries. One difficulty with this approach is that it is not always clear how to express some invariants in terms of squared distances. To that end, we present a new straightening algorithm for Euclidean invariants. We will also prove the first and second fundamental theorems of vector invariants for the group of Euclidean isometries (that the invariant subring is a finitely generated algebra over the reals, and that it can be expressed as a polynomial ring modulo finitely generated ideal, respectively. Another difficulty is that the ring of interpoint squared distances must be represented as the quotient of a polynomial ring by an ideal. Unfortunately, no canonical Gröbner basis for this ideal is known. We will present a candidate for such a basis and prove that it is a basis in some cases.This work was supported by the U.S. Army Research Office through the ACSyAm branch of the Mathematical Sciences Institute of Cornell University, Contract DA AL03-91-C-0027.