In this paper, we describe the use of the certification-trail technique as the basis of a hybrid framework for building formally verified software systems. Our technique involves formally verifying only a part of a software system; however, the technique yields a software system which still satisfies the most important correctness properties. Substantial savings in the overhead of software verification, and also in program running time, are shown to be possible in comparison to traditional methods. We apply our technique to the problem of sorting, since sorting represents one of the most basic operations in computer science, and a formally verified sorting certifier should have significant applicability. The results presented in this paper represent an enhancement of the certification-trail technique relative to the detection of incorrect computational output caused by software faults.

Resource limitations have played an important role in the development and verification of theories about intelligent behaviour. This paper is a step towards answering the question of what effect limited memory has on the ability of intelligent machines to learn from data. Our analysis is applicable to many existing learning methods, especially those that incrementally construct a generalization by making repeated passes through a set of training data (e.g. some implementations of perceptrons, neural nets, and decision trees). Most of these methods do not store the entire training set, since they allow themselves only limited storage, a restriction that forces them to produce a compressed representation. The question we address is, how much (if any) additional processing time is required for methods with limited storage ? We measure processing time for learning algorithms by the number of passes through a data set necessary to obtain a correct generalization. Researchers have observed that for some learning methods (e.g. neural nets) the number of passes through a data set gets smaller as the size of the network is increased ; however, no analytical study that explains this behaviour has been published. We examine limited storage algorithms for a particular concept class, nested hyperrectangles. We prove bounds that illustrate the fundamental trade-off between storage requirements and processing time required to learn an optimal structure. It turns out that our lower bounds apply to other algorithms and concept classes as well (e.g. decision trees). We discuss applications of our analysis to learning and to problems in human perception. We also briefly discuss parallel learning algorithms.

We describe a conceptually novel and powerful technique to achieve fault detection and fault tolerance in hardware and software systems. When used for software fault detection, this new technique uses time and software redundancy and can be outlined as follows. In the initial phase, a program is run to solve a problem and store the result. In addition, this program leaves behind a trail of data which we call a certification trail. In the second phase, another program is run which solves the original problem again. This program however, has access to the certification trail left by the first program. Because of the availability of the certification trail, the second phase can be performed by a less complex program and can execute more quickly. In the final phase, the two results are compared and if they agree the results are accepted as correct; otherwise an error is indicated. An essential aspect of this approach is that the second program must always generate either an error indication or a correct output even when the certification trail it receives from the first program is incorrect. We formalize the certification trail approach to fault tolerance and illustrate realizations of it by considering algorithms for the following problems: convex hull, sorting, and shortest path. We compare the certification trail approach to other approaches to fault tolerance.>

This paper investigates design techniques which may be applied to make program testing easier. We present methods for modifying a program to generate additional data which we refer to as a certification trail. This additional data is designed to allow the program output to be checked more quickly and effectively. Certification trails have heretofore been described primarily from a theoretical perspective. In this paper, we report on a comprehensive attempt to assess experimentally the performance and overall value of the certification trail method. The method has been applied to nine fundamental, well-known algorithms for the following problems: convex hull, sorting, huffman tree, shortest path, closest pair, line segment intersection, longest increasing subsequence, skyline, and voronoi diagram. Run-time performance data for each of these problems is given, and selected problems are described in more detail. Our results indicate that there are many cases in which certification trails allow for significantly faster overall program execution time than a two-version programming approach, and also give further evidence of the breadth of applicability of this method.>

The authors report on an attempt to assess the performance of algorithms utilizing certification trails on abstract data types. Specifically, they have applied this method to the following problems: heapsort, Huffman tree, shortest path, and skyline. Previous results used certification trails specific to a particular problem and implementation. The approach allows certification trails to be localized to data structure modules making the use of this technique transparent to the user of such modules.>

The problem of fault diagnosis in multiprocessor systems is considered under a probabilistic fault model. The focus is on minimizing the number of tests that must be conducted to correctly diagnose the state of every processor in the system with high probability. A diagnosis algorithm that can correctly diagnose these states with probability approaching one in a class of systems performing slightly greater than a linear number of tests is presented. A nearly matching lower bound on the number of tests required to achieve correct diagnosis in arbitrary systems is proved. Lower and upper bounds on the number of tests required for regular systems are presented. A class of regular systems which includes hypercubes is shown to be correctly diagnosable with high probability. In all cases, the number of tests required under this probabilistic model is shown to be significantly less than under a bounded-size fault set model. These results represent a very great improvement in the performance of system-level diagnosis techniques.>

The authors present and analyze a probabilistic model for the self-diagnosis capabilities of a multiprocessor system. In this model an individual processor fails with probability p and a nonfaulty processor testing a faulty processor detects a fault with probability q. This models the situation where processors can be intermittently faulty or the situation where tests are not capable of detecting all possible faults within a processor. An efficient algorithm that can achieve correct diagnosis with high probability in systems of O(n log n) connections, where n is the number of processors, is presented. It is the first algorithm to be able to diagnose a large number of intermittently faulty processors in a class of systems that includes hypercubes. It is shown that, under this model, no algorithm can achieve correct diagnosis with high probability in regular systems which conduct a number of tests dominated by n log n. Examples of systems which perform a modest number of tests are given in which the probability of correct diagnosis for the algorithm is very nearly one.>

The problem of voting is studied for both the exact and inexact cases. Optimal solutions based on explicit computation of condition probabilities are given. The most commonly used strategies, i.e. majority, median, and plurality are compared quantitatively. The results show that plurality voting is the most powerful of these techniques and is, in fact, optimal for a certain class of probability distributions. An efficient method of implementing a generalized plurality voter when nonfaulty processes can produce differing answers is also given.>

Consider a system of processing elements in which elements may administer tests to other elements. We show, surprisingly, that a constant number of rounds of parallel testing are sufficient to identify all faults (in all cases where fault identification is possible). We also present an O(log log n=t t) algorithm with a small constant of proportionality, where n denotes the total number of processors and t denotes the number of faulty processors. Both of these results improve upon the previous best, which was O(log n=t t) rounds. For the problems of identifying a single faulty processor (diagnosis-with-repair) and identifying a single good processor, we present an oblivious constant-time algorithm using a fixed 3-regular interconnect that tolerates a linear number of faults. This contrasts with the well-known result that every oblivious algorithm for complete diagnosis must use a number of rounds that is linear in t. 1 Introduction Consider a system composed of many processing element...

Consider a digraph which has labels on its edges which are k-dimensional vectors. In this paper we show it is possible in polynomial time to determine if such a digraph contains a zero cycle, i.e., a cycle whose edge labels sum to the zero vector component-wise. This solves the open problem of finding cycles in dynamic graphs which was posed by Iwano and Steiglitz. Our solution has a time complexity of O(|V| log(|V|)Z) where Z is the complexity of a linear programming problem. For the important cases of two and three dimensions we present O(Z) time algorithms. The linear programming problems we solve have at most 2|E| variables and O(|E| + |V| + k) constraints.

Systems composed of many processing units can use these units to help perform self-diagnosis. An algorithm is presented that performs this type of diagnosis for the system-level fault model. The time complexity of the algorithm is O(t/sup 3/+ mod E mod ), where mod E mod is the number of tests and t is the number of allowed faults. When t is small relative to the total number of system components n, this is the tightest known time bound; when t is O(n/sup 5/6/) this is the best bound.>

We present the first polynomial time algorithm for testing t-diagnosability. This is a significant advance in system level fault diagnosis. We also presented part of our analysis of t/s-diagnosability, including the fact that it is co-NP-complete and that there are polynomial algorithms for t/t and t/(t+1)-diagnosability.