VPNs (Virtual Private Networks) have become an essential privacy-enhancing technology, particularly for at-risk users like dissidents, journalists, NGOs, and others vulnerable to targeted threats. While previous research investigating VPN security has focused on cryptographic strength or traffic leakages, there remains a gap in understanding how lower-level primitives fundamental to VPN operations, like connection tracking, might undermine the security and privacy that VPNs are intended to provide. In this paper, we examine the connection tracking frameworks used in common operating systems, identifying a novel exploit primitive that we refer to as the port shadow. We use the port shadow to build four attacks against VPNs that allow an attacker to intercept and redirect encrypted traffic, de-anonymize a VPN peer, or even portscan a VPN peer behind the VPN server. We build a formal model of modern connection tracking frameworks and identify that the root cause of the port shadow lies in five shared, limited resources. Through bounded model checking, we propose and verify six mitigations in terms of enforcing process isolation. We hope our work leads to more attention on the security aspects of lower-level systems and the implications of integrating them into security-critical applications.

Algorithms for computing congruence closure of ground equations over uninterpreted symbols and interpreted symbols satisfying associativity and commutativity (AC) properties are proposed. The algorithms are based on a framework for computing a congruence closure by abstracting nonflat terms by constants as proposed first in Kapur's congruence closure algorithm (RTA97). The framework is general, flexible, and has been extended also to develop congruence closure algorithms for the cases when associative-commutative function symbols can have additional properties including idempotency, nilpotency, identities, cancellativity and group properties as well as their various combinations. Algorithms are modular; their correctness and termination proofs are simple, exploiting modularity. Unlike earlier algorithms, the proposed algorithms neither rely on complex AC compatible well-founded orderings on nonvariable terms nor need to use the associative-commutative unification and extension rules in completion for generating canonical rewrite systems for congruence closures. They are particularly suited for integrating into the Satisfiability modulo Theories (SMT) solvers. A new way to view Groebner basis algorithm for polynomial ideals with integer coefficients as a combination of the congruence closures over the AC symbol * with the identity 1 and the congruence closure over an Abelian group with + is outlined.

In this article, we enrich McCarthy’s theory of extensional arrays with a length and a maxdiff operation. As is well-known, some diff operation (i.e., some kind of difference function showing where two unequal arrays differ) is needed to keep interpolants quantifier free in array theories. Our maxdiff operation returns the max index where two arrays differ; thus, it has a univocally determined semantics. The length function is a natural complement of such a maxdiff operation and is needed to handle real arrays. Obtaining interpolation results for such a rich theory is a surprisingly hard task. We get such results via a thorough semantic analysis of the models of the theory and of their amalgamation and strong amalgamation properties. The results are modular with respect to the index theory; we show how to convert them into concrete interpolation algorithms via a hierarchical approach realizing a polynomial reduction to interpolation in linear arithmetics endowed with free function symbols.

Abstract The word problem for a finite set of ground identities is known to be decidable in polynomial time using congruence closure, and this is also the case if some of the function symbols are assumed to be commutative or defined by certain shallow identities, called strongly shallow. We show that decidability in P is preserved if we add the assumption that certain function symbolsfareextensionalin the sense that $$f(s_1,\ldots ,s_n) \mathrel {\approx }f(t_1,\ldots ,t_n)$$ f(s1,…,sn)≈f(t1,…,tn) implies $$s_1 \mathrel {\approx }t_1,\ldots ,s_n \mathrel {\approx }t_n$$ s1≈t1,…,sn≈tn . In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP.

The concept of uniform interpolant for a quantifier-free formula from a given formula with a list of symbols, while well-known in the logic literature, has been unknown to the formal methods and automated reasoning community for a long time. This concept is precisely defined. Two algorithms for computing quantifier-free uniform interpolants in the theory of equality over uninterpreted symbols (EUF) endowed with a list of symbols to be eliminated are proposed. The first algorithm is non-deterministic and generates a uniform interpolant expressed as a disjunction of conjunctions of literals, whereas the second algorithm gives a compact representation of a uniform interpolant as a conjunction of Horn clauses. Both algorithms exploit efficient dedicated DAG representations of terms. Correctness and completeness proofs are supplied, using arguments combining rewrite techniques with model theory.

Abstract In this paper, the theory of McCarthy’s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.

No abstract available.

A new efficient algorithm for computing a parametric greatest common divisor (GCD) of parametric multivariate polynomials over k[u][x] is presented. The algorithm is based on a well-known simple insight that the GCD of two multivariate polynomials (non-parametric as well as parametric) can be extracted using the generator of the quotient ideal of a polynomial with respect to the second polynomial. And, further, this generator can be obtained by computing a minimal Gröbner basis of the quotient ideal. The main attraction of this idea is that it generalizes to the parametric case for which a comprehensive Gröbner basis is constructed for the parametric quotient ideal. It is proved that in a minimal comprehensive Gröbner system of a parametric quotient ideal, each branch of specializations corresponds to a principal parametric ideal with a single generator. Using this generator, the parametric GCD of that branch is obtained by division. This algorithm does not need to consider whether parametric polynomials are primitive w.r.t. the main variable. This is in sharp contrast to two algorithms recently proposed by Nagasaka (ISSAC, 2017). The resulting algorithm is not only conceptually simple to understand but is considerably efficient. The proposed algorithm and both of Nagasaka's algorithms have been implemented in Singular (available at http://www.mmrc.iss.ac.cn/~dwang/software.html), and their performance is compared on a number of examples. For more than two polynomials, this process can be repeated by considering pairs of polynomials; the efficiency in that case becomes even more evident.

Given a basis of a parametric polynomial ideal, an algorithm is proposed to test whether it is a comprehensive Gröbner basis or not. A basis of a parametric polynomial ideal is a comprehensive Gröbner basis if and only if for every specialization of parameters in a given field, the specialization of the basis is a Gröbner basis of the associated specialized polynomial ideal. In case a basis does not check to be a comprehensive Gröbner basis, a completion algorithm for generating a comprehensive Gröbner basis from it that is patterned after Buchberger's algorithm is proposed. Its termination is proved and its correctness is established. In contrast to other algorithms for computing a comprehensive Gröbner basis which first compute a comprehensive Gröbner system and then extract a comprehensive Gröbner basis from it, the proposed algorithm computes a comprehensive Gröbner basis directly. Further, the proposed completion algorithm always computes a minimal faithful comprehensive Gröbner basis in the sense that every polynomial in the result is from the ideal as well as essential with respect to the comprehensive Gröbner basis. A prototype implementation of the algorithm has been successfully tried on many examples from the literature. An interesting and somewhat surprising outcome of using the proposed algorithm is that there are example parametric ideals for which a minimal comprehensive Gröbner basis computed by it is different from minimal comprehensive Gröbner bases computed by other algorithms in the literature.

Program invariants are important for defect detection, program verification, and program repair. However, existing techniques have limited support for important classes of invariants such as disjunctions, which express the semantics of conditional statements. We propose a method for generating disjunctive invariants over numerical domains, which are inexpressible using classical convex polyhedra. Using dynamic analysis and reformulating the problem in non-standard ``max-plus'' and ``min-plus'' algebras, our method constructs hulls over program trace points. Critically, we introduce and infer a weak class of such invariants that balances expressive power against the computational cost of generating nonconvex shapes in high dimensions.

This article describes and evaluates DIG, a dynamic invariant generator that infers invariants from observed program traces, focusing on numerical and array variables. For numerical invariants, DIG supports both nonlinear equalities and inequalities of arbitrary degree defined over numerical program variables. For array invariants, DIG generates nested relations among multidimensional array variables. These properties are nontrivial and challenging for current static and dynamic invariant analysis methods. The key difference between DIG and existing dynamic methods is its generative technique, which infers invariants directly from traces, instead of using traces to filter out predefined templates. To generate accurate invariants, DIG employs ideas and tools from the mathematical and formal methods domains, including equation solving, polyhedra construction, and theorem proving; for example, DIG represents and reasons about polynomial invariants using geometric shapes. Experimental results on 27 mathematical algorithms and an implementation of AES encryption provide evidence that DIG is effective at generating invariants for these programs.

Dynamic invariant analysis identifies likely properties over variables from observed program traces. These properties can aid programmers in refactoring, documenting, and debugging tasks by making dynamic patterns visible statically. Two useful forms of invariants involve relations among polynomials over program variables and relations among array variables. Current dynamic analysis methods support such invariants in only very limited forms. We combine mathematical techniques that have not previously been applied to this problem, namely equation solving, polyhedra construction, and SMT solving, to bring new capabilities to dynamic invariant detection. Using these methods, we show how to find equalities and inequalities among nonlinear polynomials over program variables, and linear relations among array variables of multiple dimensions. Preliminary experiments on 24 mathematical algorithms and an implementation of AES encryption provide evidence that the approach is effective at finding these invariants.

In Kapur et al (ISSAC, 2010), a new method for computing a comprehensive Grobner system of a parameterized polynomial system was proposed and its efficiency over other known methods was effectively demonstrated. Based on those insights, a new approach is proposed for computing a comprehensive Grobner basis of a parameterized polynomial system. The key new idea is not to simplify a polynomial under various specialization of its parameters, but rather keep track in the polynomial, of the power products whose coefficients vanish; this is achieved by partitioning the polynomial into two parts-nonzero part and zero part for the specialization under consideration. During the computation of a comprehensive Grobner system, for a particular branch corresponding to a specialization of parameter values, nonzero parts of the polynomials dictate the computation, i.e., computing S-polynomials as well as for simplifying a polynomial with respect to other polynomials; but the manipulations on the whole polynomials (including their zero parts) are also performed. Grobner basis computations on such pairs of polynomials can also be viewed as Grobner basis computations on a module. Once a comprehensive Grobner system is generated, both nonzero and zero parts of the polynomials are collected from every branch and the result is a faithful comprehensive Grobner basis, to mean that every polynomial in a comprehensive Grobner basis belongs to the ideal of the original parameterized polynomial system. This technique should be applicable to other algorithms for computing a comprehensive Grobner system as well, thus producing both a comprehensive Grobner system as well as a faithful comprehensive Grobner basis of a parameterized polynomial system simultaneously. The approach is exhibited by adapting the recently proposed method for computing a comprehensive Grobner system in (ISSAC, 2010) for computing a comprehensive Grobner basis. The timings on a collection of examples demonstrate that this new algorithm for computing comprehensive Grobner bases has better performance than other existing algorithms.

A number of new cryptographic protocols are being designed to secure applications such as video-conferencing and electronic voting. Many of them rely upon cryptographic functions with complex algebraic properties that must be accounted for in order to be correctly analyzed by automated tools. Maude-NPA is a cryptographic protocol analysis tool based on narrowing and typed equational unification which takes into account these algebraic properties. It has already been used to analyze protocols involving bounded associativity, modular exponentiation, and exclusive-or. All of the above can be handled by the same general variant-based equational unification technique. However, there are important properties, in particular homomorphic encryption, that cannot be handled by variant-based unification in the same way. In these cases the best available approach is to implement specialized unification algorithms and combine them within a modular framework. In this paper we describe how we apply this approach within Maude-NPA, with respect to encryption homomorphic over a free operator. We also describe the use of Maude-NPA to analyze several protocols using such an encryption operation. To the best of our knowledge, this is the first implementation of homomorphic encryption of any sort in a tool for verifying the security of a protocol in the presence of active attackers.

Modeling the semantics of programming languages like C for the automated termination analysis of programs is a challenge if complete coverage of all language features should be achieved. On the other hand, low-level intermediate languages that occur during the compilation of C programs to machine code have a much simpler semantics since most of the intricacies of C are taken care of by the compiler frontend. It is thus a promising approach to use these intermediate languages for the automated termination analysis of C programs. In this paper we present the tool KITTeL based on this approach. For this, programs in the compiler intermediate language are translated into term rewrite systems (TRSs), and the termination proof itself is then performed on the automatically generated TRS. An evaluation on a large collection of C programs shows the effectiveness and practicality of KITTeL on "typical" examples.

A new algorithm for computing a comprehensive Gröbner system of a parametric polynomial ideal over k[U][X] is presented. This algorithm generates fewer branches (segments) compared to Suzuki and Sato's algorithm as well as Nabeshima's algorithm, resulting in considerable efficiency. As a result, the algorithm is able to compute comprehensive Gröbner systems of parametric polynomial ideals arising from applications which have been beyond the reach of other well known algorithms. The starting point of the new algorithm is Weispfenning's algorithm with a key insight by Suzuki and Sato who proposed computing first a Gröbner basis of an ideal over k[U,X] before performing any branches based on parametric constraints. Based on Kalkbrener's results about stability and specialization of Gröbner basis of ideals, the proposed algorithm exploits the result that along any branch in a tree corresponding to a comprehensive Gröbner system, it is only necessary to consider one polynomial for each nondivisible leading power product in k(U)[X] with the condition that the product of their leading coefficients is not 0; other branches correspond to the cases where this product is 0. In addition, for dealing with a disequality parametric constraint, a probabilistic check is employed for radical membership test of an ideal of parametric constraints. This is in contrast to a general expensive check based on Rabinovitch's trick using a new variable as in Nabeshima's algorithm. The proposed algorithm has been implemented in Magma and experimented with a number of examples from different applications. Its performance (vis a vie number of branches and execution timings) has been compared with the Suzuki-Sato's algorithm and Nabeshima's speed-up algorithm. The algorithm has been successfully used to solve the famous P3P problem from computer vision.

This paper introduces a novel set of heuristics for identifying logically related sections of the heap such as recursive data structures, objects that are part of the same multi-component structure, and related groups of objects stored in the same collection/array. When combined with lifetime properties of these structures, this information can be used to drive a range of program optimizations including pool allocation, object co-location, static deallocation, and region-based garbage collection. The technique outlined in this paper also improves the efficiency of the static analysis by providing a compact normal form for the abstract models (speeding the convergence of the static analysis).

Precise modeling of the program heap is fundamental for understanding the behavior of a program, and is thus of significant interest for many optimization applications. One of the fundamental properties of the heap that can be used in a range of optimization techniques is the sharing relationships between the elements in an array or collection. If an analysis can determine that the memory locations pointed to by different entries of an array (or collection) are disjoint, then in many cases loops that traverse the array can be vectorized or transformed into a thread-parallel version. This paper introduces several novel sharing properties over the concrete heap and corresponding abstractions to represent them. In conjunction with an existing shape analysis technique, these abstractions allow us to precisely resolve the sharing relations in a wide range of heap structures (arrays, collections, recursive data structures, composite heap structures) in a computationally efficient manner. The effectiveness of the approach is evaluated on a set of challenge problems from the JOlden and SPECjvm98 suites. Sharing information obtained from the analysis is used to achieve substantial thread-level parallel speedups.

Memory analysis techniques have become sophisticated enough to model, with a high degree of accuracy, the manipulation of simple memory structures (finite structures, single/double linked lists and trees). However, modern programming languages provide extensive library support including a wide range of generic collection objects that make use of complex internal data structures. While these data structures ensure that the collections are efficient, often these representations cannot be effectively modeled by existing methods (either due to excessive analysis runtime or due to the inability to represent the required information). This paper presents a method to represent collections using an abstraction of their semantics. The construction of the abstract semantics for the collection objects is done in a manner that allows individual elements in the collections to be identified. Our construction also supports iterators over the collections and is able to model the position of the iterators with respect to the elements in the collection. By ordering the contents of the collection based on the iterator position, the model can represent a notion of progress when iteratively manipulating the contents of a collection. These features allow strong updates to the individual elements in the collection as well as strong updates over the collections themselves.

Matrices constructed from a parameterized multivariate polynomial system are analyzed to ensure that such a matrix contains a condition for the polynomial system to have common solutions irrespective of whether its parameters are specialized or not. Such matrices include resultant matrices constructed using well-known methods for computing resultants over projective, toric and affine varieties. Conditions on these matrices are identified under which the determinant of a maximal minor of such a matrix is a nontrivial multiple of the resultant over a given variety. This condition on matrices allows a generalization of a linear algebra construction, called rank submatrix, for extracting resultants from singular resultant matrices, as proposed by Kapur, Saxena and Yang in ISSAC'94. This construction has been found crucial for computing resultants of non-generic, specialized multivariate polynomial systems that arise in practical applications. The new condition makes the rank submatrix construction based on maximal minor more widely applicable by not requiring that the singular resultant matrix have a column independent of the remaining columns. Unlike perturbation methods, which require introducing a new variable, rank submatrix construction is faster and effective. Properties and conditions on symbolic matrices constructed from a polynomial system are discussed so that the resultant can be computed as a factor of the determinant of a maximal non-singular submatrix.

Interpolation based automatic abstraction is a powerful and robust technique for the automated analysis of hardware and software systems. Its use has however been limited to control-dominated applications because of a lack of algorithms for computing interpolants for data structures used in software programs. We present efficient procedures to construct interpolants for the theories of arrays, sets, and multisets using the reduction approach for obtaining decision procedures for complex data structures. The approach taken is that of reducing the theories of such data structures to the theories of equality and linear arithmetic for which efficient interpolating decision procedures exist. This enables interpolation based techniques to be applied to proving properties of programs that manipulate these data structures.

A geometric concept of the support hull of the support of a polynomial was used earlier by the authors for developing a tight upper bound on the size of the Cayley-Dixon resultant matrix for an unmixed polynomial system. The relationship between the support hull and the Cayley-Dixon resultant construction is analyzed in this paper. The support hull is shown to play an important role in the construction and analysis of resultant matrices based on the Cayley-Dixon formulation, similar to the role played by the associated convex hull (Newton polytope) for analyzing resultant matrices over the toric variety. For an unmixed polynomial system, the sizes of the resultant matrices (both dialytic as well as nondialytic) constructed using the Cayley-Dixon formulation are determined by the support hull of its support. Consequently, degree of the projection operator (which is in general, a nontrivial multiple of the resultant) computed from such a resultant matrix is determined by the support hull.The support hull of a given support is similar to its convex hull except that instead of the Euclidean distance, the support hull is defined using rectilinear distance. The concept of a support-hull interior point is introduced. It is proved that for an unmixed polynomial system, the size of the resultant matrix (both dialytic and nondialytic) based on the Cayley-Dixon formulation remains the same even if a term whose exponent is support-hull interior with respect to the support is generically added to the polynomial system. This key insight turned out to be instrumental in generalizing the concept of an unmixed polynomial system with a corner-cut support from 2 dimensions to arbitrary dimension as well as identifying an unmixed polynomial system with almost corner-cut support in arbitrary dimension.An algorithm for computing the size (and the lattice points) of the support hull of a given support is presented. It is proved that determining whether a given lattice point is not in the support hull, is NP-complete. A heuristic for computing a good variable ordering for constructing Dixon matrices for mixed as well as unmixed polynomial systems is proposed using the support hull and its projections. This is one of the first results on developing heuristics for variable orderings for constructing resultant matrices. A construction for a Sylvester-type resultant matrix based on the support hull of a polynomial system is also given.

This paper presents the algebraic foundation for an approach for generating polynomial loop invariants in imperative programs. It is first shown that the set of polynomials serving as loop invariants has the algebraic structure of an ideal. Using this connection, a procedure for finding loop invariants is given in terms of operations on ideals, for which Grobner basis constructions can be employed. Most importantly, it is proved that if the assignment statements in a loop are solvable (in particular, affine) mappings with positive eigenvalues, then the procedure terminates in at most 2m+1 iterations, where m is the number of variables in the loop. The proof is done by showing that the irreducible subvarieties of the variety associated with the polynomial ideal approximating the invariant polynomial ideal of the loop either stay the same or increase their dimension in every iteration. This yields a correct and complete algorithm for inferring conjunctions of polynomial equations as invariants. The method has been implemented in Maple using the Groebner package. The implementation has been used to automatically discover nontrivial invariants for several examples to illustrate the power of the techniques.

Structural conditions on polynomial systems are developed for which the Dixon-based resultant methods often compute exact resultants. For cases when this cannot be done, the degree of the extraneous factor in the projection operator computed using the Dixon-based methods is typically minimal. A method for constructing a resultant matrix based on a combination of Sylvester-dialytic and Dixon methods is proposed. A heuristic for variable ordering for this construction often leading to exact resultants is developed.

A structural criteria on polynomial systems is developed for which the generalized Dixon formulation of multivariate resultants defined by Kapur, Saxena and Yang (1994) computes the resultant exactly. The concept of a Dixon-exact support (the set of exponent vectors of terms appearing in a polynomial system) is introduced so that the Dixon formulation produces the exact resultant for generic unmixed polynomial systems whose support is Dixon-exact. A geometric operation, called direct-sum, on the supports is defined that preserves the property of supports being Dixon-exact. Generic n-degree systems and multigraded systems are shown to be a special case of generic unmixed polynomial systems whose support is Dixon-exact. Using a scaling techniques discussed by Kapur and Saxena (1997), a wide class of polynomial systems can be identified for which the Dixon formulation produces exact resultants. This analysis can be used to classify terms appearing in the convex hull (also called the Newton polytope) of the support of a polynomial system that can cause extraneous factors in the computation of a projection operation by the generalized Dixon formulation. For the bivariate case, a complete analysis of the terms corresponding to the exponent vectors in the Newton polytope of the support of a polynomial system is given vis a vis their role in producing extraneous factors in a projection operator. A necessary and sufficient condition is developed for a support to be Dixon-exact. Such an analysis is likely to give insights for the general case of elimination of arbitrarily many variables.

Elimination methods based on generalizations of the Dixon's resultant formulation have been demonstrated to be efficient for simultaneously eliminating many variables from polynomials. One of these methods, presented by the authors earlier, was even shown to exploit the sparse structure of a polynomial system as determined by its Newton polytope. This paper analyzes the extraneous factors in the projection operators computed by that method. It is shown that the projection operator of a polynomial system can be related to the projection operator of another system consisting of polynomials with smaller Newton polytopes and lower degrees, thus making resultant computation more efficient. If a larger polyomial system can be obtained from another smaller one by replacing variables by their powers, then the projection operator of the larger system is proved to be a power of the projection operator of the smaller one. This shows that the set of extraneous factors in the two projection operato...

Many parallel applications are designed to conceal parallelism from the user. We investigate a different approach where the user controls many tasks running in parallel. The idea is to let a user accomplish his goal more quickly by trying competing alternatives in parallel (or-parallelism) and by working on subgoals in parallel (and-parallelism). To help the user manage a large number of parallel tasks, the application must provide features to generate many tasks easily, to summarize the state of all tasks, to broadcast commands to related tasks, and to abort tasks that are no longer needed. A parallel interface to an application thus becomes crucial to enhance the user's productivity. We demonstrate this approach using DLP, a parallel, distributed version of the Larch Prover, an interactive theorem prover. DLP supports explicit parallelism and runs on a network of workstations. Users control DLP through a multi-window interface on a bit-map color-display. Many theorem proving problems that would otherwise take considerable user effort to solve have been done with relative ease using DLP.

New results relating the sparsity of nonhomogeneous polynomial systems and computation of their projection operator (a non-trivial multiple of the multivariate resultant) using Dixon's method are developed. It is demonstrated that Dixon's method of computing resultants, despite being classical, implicitly exploits the sparse structure of input polynomials. It is proved that the size of the Dixon matrix, and the complexity of computing the resultant using Dixon's method is not determined by the total degree of the polynomial system, but rather by the structure of the Newton polytopes of the polynomial system. An exact formula for the size of the Dixon matrix of unmixed polynomial systems is derived in terms of their Newton polytopes. This relationship is exploited to tightly bound the size of the Dixon matrices of multi-homogeneous polynomial systems and also to devise an algorithm for constructing their Dixon matrices efficiently using dense polynomial interpolation. This work links th...

Three most important resultant formulations are the Macaulay, Dixon and sparse resultant formulations. For most polynomial systems, however, the matrices constructed in these formulations become singular and the projection operator vanishes identically. In such cases, perturbation techniques for Macaulay formulation such as generalized characteristic polynomial (GCP) and a method based on rank submatrix computation (RSC), applicable to all three formulations, can be used, giving four methods, Macaulay/GCP, Macaulay/RSC, Dixon/RSC and Sparse/RSC, for computing nontrivial projection operators. In this paper, these four methods are compared. It is shown that the Dixon matrix is (by a factor up to O(e n ) for a certain class) smaller than the sparse resultant matrix which is (by a factor up to O(e n ) for a certain class) smaller than the Macaulay matrix. Empirical results confirm that Dixon/RSC is the most efficient, followed by Sparse/RSC then Macaulay/RSC and finally Macaulay/GCP, ...

Dixon's method for computing multivariate resultants by simultaneously eliminating many variables is reviewed. The method is found to be quite restrictive because often the Dixon matrix is singular, and the Dixon resultant vanished identically yielding no information about solutions for many algebraic and geometry problems. We extend Dixon's method for the case when the Dixon matrix is singular, but satisfies a condition. An efficient algorithm is developed based on the proposed extension for extracting conditions for the existence of affine solutions of a finite set of polynomials. Using this algorithm, numerous geometric and algebraic identities are derived for examples which appear intractable with other techniques of triangulation such as the successive resultant method, the Gro¨bner basis method, Macaulay resultants and Characteristic set method. Experimental results suggest that the resultant of a set of polynomials which are symmetric in the variables is relatively easier to compute using the extended Dixon's method.

Books on software engineering methodologies talk about the significance and need for designing consistent and complete specifications during the requirement analysis and design stages of a software development cycle. There is, however, little (or at best very limited) discussion of methods for ensuring these structural properties of specifications. In this paper, we discuss methods for checking completeness of equational specifications. Some of these methods were earlier proposed in somewhat different form in the context of developing the so-called inductionless induction method for automating proofs by induction using completion procedures. These methods are implemented in our theorem prover Rewrite Rule Laboratory (RRL), and have been tried on a number of examples of specifications of data abstractions. In case a specification is incomplete, these methods can aid in making them complete by generating templates which are not specified. Templates can also be helpful in distinguishing between intentional and unintentional incompleteness in specifications. Further, these methods can be used to generate test cases for checking specifications and verifying implementations of specifications. These methods are illustrated on examples which exhibit their power as well as limitations.

An algorithm for computing a complete set of unifiers for two terms involving associative-commutative function symbols is presented. It is based on a nondeterministic algorithm given by the authors in 1986 to show the NP-completeness of associative-commutative unifiability. The algorithm is easy to understand, and its termination can be easily established. Its complexity is easily analyzed and shown to be doubly exponential in the size of the input terms. The analysis also shows that there is a double-exponential upper bound on the size of a complete set of unifiers of two input terms. Since there is a family of simple associative-commutative unification problems which have complete sets of unifiers whose size is doubly exponential, the algorithm is optimal in its order of complexity in this sense.>

A generic polyhedral model is represented as a network of nodes and constraints. Nodes are 3-D vectors representing the location and orientation of the geometric entities, or measure variables such as length or cosine. Constraints are polynomial equations in the node parameters. Modeling and recognition are viewed as solving for values of the node parameters such that all the constraint equations are satisfied and the mean square error between the model and the observed shape is minimized. Buchberger's Grobner basis algorithm and Ritt-Wu's triangulation algorithm can be used for eliminating dependent parameters as well as for detecting inconsistency among constraints. Numerical techniques are used to find the best-fit model subject to constraints.>

A refutational approach to geometry theorem proving using Ritt-Wu's algorithm for computing a characteristic set is discussed. A geometry problem is specified as a quantifier-free formula consisting of a finite set of hypotheses implying a conclusion, where each hypothesis is either a geometry relation or a subsidiary condition ruling out degenerate cases, and the conclusion is another geometry relation. The conclusion is negated, and each of the hypotheses (including the subsidiary conditions) and the negated conclusion is converted to a polynomial equation. Characteristic set computation is used for checking the inconsistency of a finite set of polynomial equations over an algebraic closed field. The method is contrasted with a related refutational method that used Buchberger's Gröbner basis algorithm for the inconsistency check.

The use of formal geometric reasoning is proposed to analyze algorithms for machine vision and robotics. This paper develops the basis for this approach and illustrates the method with several examples taken from perspective scene analysis. The application of recent developments in algebraic deduction methods is described.

The Knuth-Bendix completion procedure for term rewriting systems in many cases provides a decision procedure for equational theories and has been found to have many applications in various areas. We discuss the application of the Knuth-Bendix procedure to Thue systems. We use the notion of a reduced Thue system and show that for every Church-Rosser Thue system, there is a unique reduced Church-Rosser Thue system equivalent to it. Furthermore, the Knuth-Bendix completion procedure, when applied to a Thue system T, always produces the finite reduced Church-Rosser Thue system equivalent to T whenever such a system exists. Similar results can also be proved for almost-confluent Thue systems. Using properties of reduced Church-Rosser systems, we develop conditions under which a class of special Thue systems have equivalent finite Church-Rosser systems. In addition, we show that the completion procedure always terminates on finite parenthesized Thue systems, from which the termination of the completion procedure over ground-term-rewriting systems can be shown immediately. From the results discussed in this paper, we also obtain the termination of the Knuth-Bendix completion procedure for commutative Thue systems (commutative monoids) as a simple corollary.

In mechanical theorem proving, particularly in proving properties of algebraically specified data types, we frequently need a decision procedure for the theory of a given finite set of equations (axioms). A general approach to this problem is to try to derive from the axioms a set of rewrite rules that are “canonical,” i.e., they rewrite to a canonical form all terms that are equal (according the axioms and the equivalence and substitution properties of equality). Rewrite rules are canonical if and only if they determine a relation that is both confluent and uniformly terminating. The difficulty of proving uniform termination has been the major drawback of the rewrite rule approach to deciding equations. A new method of proving uniform termination is proposed. Assuming that the rewriting relation is globally finite (for any term there are only finitely many terms to which it can be rewritten), nontermination can occur only if there are cycles. Uniform termination is proved by showing that no cycles can occur. A method related to the Knuth and Bendix method of proving confluence is developed and used as the basis of such proof. In most cases, the proposed method will only prove termination for terms up to a certain size; this kind of “restricted termination” has a number of applications.

In a strongly typed system supporting user defined data abstractions, the designer of a data abstraction ought to be careful in choosing the operations for the abstraction. If the operation set chosen is not expressive enough, it might be impossible or inconvenient to implement certain useful functions on the values of the data abstraction. In this paper, we characterize the expressive power of the operation set by defining two properties for data abstractions - expressive completeness and expressive richness. The operation set of an expressively complete data abstraction is adequate enough to implement all computable functions on its values. An expressively rich data abstraction is expressively complete with an operation set that is rich enough to conveniently extract from a value, all relevant information required to reconstruct the value from scratch. Practical applications of the properties of expressiveness introduced are also discussed.