The central paradigm of today's successful Internet is to keep the network core simple and move complexity towards the network end points. Unfortunately, this very paradigm limits network management and control capabilities, and creates opportunities for attacks such as worms, viruses, and spam that often seriously disrupt and degrade Internet and user performance. The thrust of this paper is that such problems cannot be effectively solved unless a paradigm shift is adopted. Towards a more secure and manageable Internet, we propose "virtualization" of the Internet, by carefully balancing its scalability and programmability properties. Our objective is to provide a programmable virtual Internet to users and to let them manage, control, and optimize it based on their individual needs.

Quicksort is the preferred in-place sorting algorithm in many contexts, since its average computing time on uniformly distributed inputs is Θ(N log N), and it is in fact faster than most other sorting algorithms on most inputs. Its drawback is that its worst-case time bound is Θ(N2). Previous attempts to protect against the worst case by improving the way quicksort chooses pivot elements for partitioning have increased the average computing time too much – one might as well use heapsort, which has a Θ(N log N) worst-case time bound, but is on the average 2–5 times slower than quicksort. A similar dilemma exists with selection algorithms (for finding the i-th largest element) based on partitioning. This paper describes a simple solution to this dilemma: limit the depth of partitioning, and for subproblems that exceed the limit switch to another algorithm with a better worst-case bound. Using heapsort as the ‘stopper’ yields a sorting algorithm that is just as fast as quicksort in the average case, but also has an Θ(N log N) worst case time bound. For selection, a hybrid of Hoare's FIND algorithm, which is linear on average but quadratic in the worst case, and the Blum–Floyd–Pratt–Rivest–Tarjan algorithm is as fast as Hoare's algorithm in practice, yet has a linear worst-case time bound. Also discussed are issues of implementing the new algorithms as generic algorithms, and accurately measuring their performance in the framework of the C+:+ Standard Template Library. ©1997 by John Wiley & Sons, Ltd.

Dynamic verification is a new approach to formal verification, applicable to generic algorithms such as those found in the Standard Template Library (STL, part of the Draft ANSI/ISO C++ Standard Library). Using behavioral abstraction and symbolic execution techniques, verifications are carried out at an abstract level such that the results can be used in a variety of instances of the generic algorithms without repeating the proofs. This is achieved by substituting for type parameters of generic algorithms special data types that model generic concepts by accepting symbolic inputs and deducing outputs using inference methods. By itself, this symbolic execution technique supports testing of programs with symbolic values at an abstract level. For formal verification one also needs to generate multiple program execution paths and use assertions (to handle while loops, for example), but the authors show how this can be achieved via directives to a conventional debugger program and an analysis database. The assertions must still be supplied, but they can be packaged separately and evaluated as needed by appropriate transfers of control orchestrated via the debugger. Unlike all previous verification methods, the dynamic verification method thus works without having to transform source code or process it with special interpreters. They include an example of the formal verification of an STL generic algorithm.

Given a vector space basis with integral domain coefficients, a variant of the Gram-Schmidt process produces an orthogonal basis using exact divisions, so that all arithmetic is within the integral domain. Zero-division is avoided by the assumption that in the domain a sum of squares of nonzero elements is always nonzero. In this paper we fully develop this method and use it to illustrate and compare a variety of means for implementing generic algorithms. Previous generic programming methods have been limited to one of compile-time, link-time, or run-time instantiation of type parameters, such as the integral domain of this algorithm, but we show how to express generic algorithms in C+ + so that all three possibilities are available using a single source code. Finally, we take advantage of the genericness to test and time the algorithm using different arithmetics, including three huge-integer arithmetic packages. 1 Introduction Given a basis B = fb1 ; : : : ; bng for R n the Gram-S...

Abstract We outline an approach to construction of software libraries in which generic algorithms (algorithmic abstractions) play a more central role than in conventional software library technology or in the object‐oriented programming paradigm. Our approach is to consider algorithms first, decide what types and access operations they need for efficient execution, and regard the types and operations as formal parameters that can be instantiated in many different ways, as long as the actual parameters satisfy the assumptions on which the correctness and efficiency of the algorithms are based. The means by which instantiation is carried out is language dependent; in the C + + examples in this paper, we instantiate generic algorithms by constructing classes that define the needed types and access operations. By use of such compile‐time techniques and careful attention to algorithmic issues, it is possible to construct software components of broad utility with no sacrifice of efficiency.

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.

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.

A class of univariate polynomials is defined which make the Berlekamp-Hensel factorization algorithm take an exponential amount of time. This class contains as subclasses the Swinnerton-Dyer polynomials discussed by Berlekamp and a subset of the cyclotomic polynomials. Aside from shedding light on the complexity of polynomial factorization this class is also useful in testing implementations of the Berlekamp–Hensel and related algorithms.

The equational axioms of an algebraic specification of a data type (such as finite sequences) often can be formed into a convergent set of rewrite rules; i.e. such that all sequences of rewrites are finite and uniquely terminating. If one adds a rewrite rule corresponding to a data type property whose proof requires induction (such as associativity of sequence concatenation), convergence may be destroyed, but often can be restored by using the Knuth-Bendix algorithm to generate additional rules. A convergent set of rules thus obtained can be used as a decision procedure for the equational theory for the axioms plus the property added. This fact, combined with a "full specification" property of axiomatizations, leads to a new method of proof of inductive properties--not requiring the explicit invocation of an inductive rule of inference.

This paper describes the data type definition facilities of the AFFIRM system for program specification and verification. Following an overview of the system, we review the rewrite rule concepts that form the theoretical basis for its data type facilities. The main emphasis is on methods of ensuring convergence (finite and unique termination) of sets of rewrite rules and on the relation of this property to the equational and inductive proof theories of data types.

An important part of a previously given algorithm for factonng integral polynomials (D R Musser, Multivariate polynomial factonzation, J ACM 22, 2, April 1975) is a test for irreducibility based on mod p factonzations for several different prime mtegers p This paper analyzes the average efficiency of this test by determining the mean number of primes required to establish irreducibility of a random input polynomial.Tables are given showing this mean as a function of the degree of the mpnt polynomial, for degrees ranging up to 200 These tables were constructed in part usmg a Markov chain model of the behavior of the irreducibility test algonthm, and m part usmg an efficient simulation of the algorithm.The results show that the mean number of pnrnes grows very slowly with the degree and is less than 5 for all degrees up to 200 The Markov chain model and simulation model exploit an mterestmg correspondence between the factor structure of random polynomials over fmlte fields and the cycle structure of random permutations KEY WORDS AND PHRASES polynomial factoring, irreducibility test, average computing time, Markov chain, combinational enumeration CR CATEGORIES 5.25, 5 39, 5 7 n = 10 and that modulo p = 2 we obtain three irreducible factors of A(x) of degrees 2, 2, 6.Then Dp = {0, 2, 4, 6, 8, 10}.If the modulo q --3 irreducible factors have degrees 3, 3, 4 then Dq --{0, 3, 4, 6, 7, 10} and Dp N Dq --{0, 4, 6, 10}.If the modulo r --5 irreducible factors have degrees 2, 3, 5 then Dr = {0, 2, 3, 5, 7, 8, 10} and D, N Dq N Dr = {0, 10}, proving A(x) nrreducible.This "degree compatibility testing" method was included by the author in a computer algorithm for factoring integral polynomials described m [12,6,13].The modulo p factofizations are performed using the "distinct degree factorization" algorithm described in [11, p. 389] and [5].This algorithm produces only a partial factorization, but yields enough information to determine the degrees of all irreducible factors.One of Berlekamp's algorithms [ 1,2] for complete factorization could also be used.The maximum time required General permission to make fair use in teachmg or research of all or part of this matenal is granted to individual readers and to nonprofit hbranes acting for them provided that ACM's copyright notice is given and that reference Is made to the publication, to ItS date of issue, and to the fact that reprmtmg pnvfleges were granted by permission of the Association for Computmg Machmery.To otherwise repnnt a figure, table, other substantial excerpt, or the entire work requires specific permission as does republication, or systematic or multiple reproduction.

This paper describes algorithms for factoring a polynomial in one or more variables, with integer coefficients, into factors which are irreducible over the integers These algorithms are based on the use of factorIzatmns over finite fields and "Hensel's lemma constructions " "Abstract algorithm" descripttons are used m the presentation of the underlying algebra:c theory Included ~s a new generahzatmn of Hensel's p-adlc constructmn which leads to a practical algorithm for factorlng multivariate polynommls The univarmte case algorithm is also specified m greater deta:l than in the prewous literature, with attentmn to a number of improvements wh:ch the author has developed based OR theoretical computing time analyses and experience with actual implementatmns

Since the publication of the Curriculum 68 report of the ACM Committee [CUR 68], undergraduate computer science programs have undergone substantial changes. Notably, many courses previously taught at the graduate level have shifted down to the undergraduate level; new areas have developed and consolidated but were not covered by the ACM report. These facts make it necessary to revise and update the Curriculum 68 report. An important factor which could help the revision is the actual experience gained through the development of many new undergraduate computer science programs since the publication of Curriculum 68 report five years ago. More specifically, most recommendations of the ACM report contain just the subject areas to be taught. The actual teaching experiences of these courses have formulated certain basic philosophies and formats of presentation. It is helpful, in our opinion, to compare the merits of these philosophies and formats of presentation.