Open Access. Powered by Scholars. Published by Universities.®
- Discipline
-
- Engineering (440)
- Electrical and Computer Engineering (335)
- Numerical Analysis and Scientific Computing (104)
- Operations Research, Systems Engineering and Industrial Engineering (87)
- Physics (50)
-
- Artificial Intelligence and Robotics (47)
- Mechanical Engineering (45)
- Business (40)
- Statistics and Probability (36)
- Mathematics (34)
- Aerospace Engineering (33)
- Medicine and Health Sciences (28)
- Earth Sciences (22)
- Geology (20)
- Chemistry (18)
- Databases and Information Systems (17)
- Life Sciences (17)
- Systems Architecture (17)
- Other Computer Sciences (16)
- Power and Energy (16)
- Mining Engineering (15)
- Computer Engineering (14)
- Civil and Environmental Engineering (12)
- Social and Behavioral Sciences (12)
- Biology (11)
- Systems Engineering (11)
- Materials Science and Engineering (10)
- Psychology (8)
- Keyword
-
- Security (30)
- Clustering (19)
- Deep learning (19)
- Deep Learning (16)
- Machine Learning (16)
-
- Neural networks (16)
- Optimal control (16)
- Reinforcement learning (16)
- Federated learning (15)
- IoT (15)
- Neurocontrollers (15)
- Impact Ionization (14)
- Neural Networks (14)
- Optimization (13)
- Adaptive Control (12)
- Algorithms (12)
- Artificial Intelligence (11)
- Cloud computing (11)
- Edge computing (11)
- Internet (11)
- Wireless sensor networks (11)
- Closed Loop Systems (10)
- Lyapunov Methods (10)
- Optimal Control (10)
- Routing (10)
- Sensor networks (10)
- Anomaly detection (9)
- Ionization (9)
- Neural Network (9)
- Privacy (9)
- Publication Year
- Publication
-
- Computer Science Faculty Research & Creative Works (919)
- Electrical and Computer Engineering Faculty Research & Creative Works (282)
- Masters Theses (220)
- Computer Science Technical Reports (196)
- Doctoral Dissertations (106)
-
- Physics Faculty Research & Creative Works (44)
- Business and Information Technology Faculty Research & Creative Works (24)
- Geosciences and Geological and Petroleum Engineering Faculty Research & Creative Works (20)
- Mechanical and Aerospace Engineering Faculty Research & Creative Works (17)
- Miners Solving for Tomorrow Research Conference (16)
- Chemistry Faculty Research & Creative Works (15)
- Engineering Management and Systems Engineering Faculty Research & Creative Works (12)
- Opportunities for Undergraduate Research Experience Program (OURE) (12)
- Missouri S&T’s Peer to Peer (11)
- Undergraduate Research Conference at Missouri S&T (10)
- Materials Science and Engineering Faculty Research & Creative Works (7)
- Mathematics and Statistics Faculty Research & Creative Works (7)
- Civil, Architectural and Environmental Engineering Faculty Research & Creative Works (4)
- Mining Engineering Faculty Research & Creative Works (4)
- Biological Sciences Faculty Research & Creative Works (3)
- Chemical and Biochemical Engineering Faculty Research & Creative Works (2)
- Economics Faculty Research & Creative Works (2)
- Graduate Student Research & Creative Works (2)
- AOER Course Materials (1)
- Capstone Projects (1)
- Psychological Science Faculty Research & Creative Works (1)
- Publication Type
Articles 1711 - 1740 of 1938
Full-Text Articles in Computer Sciences
The Identification And Processing Of Don't-Care Attribute Values In Id3 Decision Tree Construction, P. D. Dorr, D. C. St. Clair
The Identification And Processing Of Don't-Care Attribute Values In Id3 Decision Tree Construction, P. D. Dorr, D. C. St. Clair
Computer Science Technical Reports
ID3 is most successful when used with sets of training and testing data that contain no missing attribute values. Many times, however, real-world domains have attributes with missing values. Sometimes these attribute values may not be needed to classify an instance. Such attribute values are called don't-care attribute values. In other cases, the values are needed but are unavailable. These values are called unknown attribute values. This paper describes the difference between unknown and don't-care attribute values and discusses several ways of identifying don't-care attribute values in ID3. Numerical results are described which validate the practicality of these approaches.
Network Key Management In A Large Distributed Environment, J. J. Stapleton, D. C. St. Clair
Network Key Management In A Large Distributed Environment, J. J. Stapleton, D. C. St. Clair
Computer Science Technical Reports
The technique of using encryption for protecting information in a network environment involves managing encryption keys within that same network. In large distributed networks the goal of achieving a secure environment requires a secure method of performing network key management. Network security, system security, and application security by means of data encryption rely on encryption keys remaining secret.
Both international and domestic standards organizations such as the International Organization for Standardization (ISO), the American National Standards Institute (ANSI), and the National Institute of Standards and Technology (NIST) address the issues of encryption through various standards. However, these standards discuss methods …
An Enhanced Reconfigurable Embedding Scheme For Rings In Hypercubes, Junlin Liu, Bruce M. Mcmillin
An Enhanced Reconfigurable Embedding Scheme For Rings In Hypercubes, Junlin Liu, Bruce M. Mcmillin
Computer Science Technical Reports
In this paper we present an enhanced version of a reported reconfigurable embedding scheme (i.e., DC scheme) that based on the idea of divide and conquer to efficiently embed even length rings in hypercubes. It was shown that the system with the DC scheme is 3-step recoverable and needs an average of 1.3 steps to recover one single fault. Here, we show that the system with the enhanced embedding scheme will be 2-step recoverable when the dimensions of hypercubes are ~ 5, and the system is able to recover any single fault in an average of 1.1 steps.
Relaxing Synchronization In Distributed Simulated Annealing, Chul-Eui Hong, Bruce M. Mcmillin
Relaxing Synchronization In Distributed Simulated Annealing, Chul-Eui Hong, Bruce M. Mcmillin
Computer Science Technical Reports
Simulated annealing is an attractive, but expensive, heuristic for approximating the solution to combinatorial optimization problems. Attempts to parallelize simulated annealing, particularly on distributed memory multicomputers, are hampered by the algorithm's requirement of a globally consistent system state. In a multicomputer, maintaining the global state S Involves explicit message traffic and is a critical performance bottleneck. To mitigate this bottleneck, it becomes necessary to amortize the overhead of these state updates over as many parallel state changes as possible. By using this technique, errors in the actual cost C(S) of a particular state S will be introduced into the annealing …
An Algorithm For Generating Executable Assertions For Fault Tolerance, Martina Schollmeyer, Hanan Lutfiyya, Bruce M. Mcmillin
An Algorithm For Generating Executable Assertions For Fault Tolerance, Martina Schollmeyer, Hanan Lutfiyya, Bruce M. Mcmillin
Computer Science Technical Reports
This paper presents an algorithm for deriving executable assertions that can be evaluated in a faulty distributed environment. A transformation from the global auxiliary variable approach into a new proof system based on the history of the auxiliary variables is introduced. This transformation, which matches the operational distributed environment more closely than the global auxiliary variable system, is then shown to retain the properties of this system such as noninterference, satisfaction, soundness, and completeness. An example is presented in which a model problem is transformed from one system into the other.
Fault-Tolerant Distributed Database Lock Managers Formally Derived From Program Verification, Hanan Lutfiyya, Martina Schollmeyer, Bruce M. Mcmillin
Fault-Tolerant Distributed Database Lock Managers Formally Derived From Program Verification, Hanan Lutfiyya, Martina Schollmeyer, Bruce M. Mcmillin
Computer Science Technical Reports
This paper presents a system for formally deriving executable assertions that can be evaluated in the faulty distributed computing environment. Since executable assertions for fault tolerance need to show that a program meets its specification and, since program verification is the process of formally showing that a program satisfies some particular properties with respect to its specification, we use program verification as a basis for derivation. It is well known that in the sequential computing environment the assertions from a program verification proof outline may be translated directly into executable assertions. However, due to the lack of global state information …
Fault-Tolerant Concurrent Branch And Bound Algorithm Derived From Program Verification, Hanan Lutfiyya, Aggie Sun, Bruce M. Mcmillin
Fault-Tolerant Concurrent Branch And Bound Algorithm Derived From Program Verification, Hanan Lutfiyya, Aggie Sun, Bruce M. Mcmillin
Computer Science Technical Reports
The process of showing that a program satisfies some particular properties with respect to its specification is called program verification. Axiomatic semantics is a verification method that makes assertions describing properties about the states of the program. There exists a transformation from the assertions of the verification proof of a program to executable assertions. These executable assertions may be embedded in the program to create a fault-tolerant program. While this approach has been applied to the sequential programming environment, the distributed programming environment presents special challenges. This paper focuses on applying concurrent programming axiomatic proof systems to generate executable assertions …
A Divide And Conquer Ring Embedding Scheme On Hypercubes With Efficient Recovery Ability, Junlin Liu, Bruce M. Mcmillin
A Divide And Conquer Ring Embedding Scheme On Hypercubes With Efficient Recovery Ability, Junlin Liu, Bruce M. Mcmillin
Computer Science Technical Reports
The hypercube architecture has been considered a useful host to simulate many networks. However, when processors on hypercubes become faulty, the simulated topologies may no longer be valid and, thus, the system needs to invoke some reconfiguration algorithm to recover the topology. The efficiency of this reconfiguration depends heavily on the initial embedding method. This paper proposes a general scheme based on the idea of divide and conquer that efficiently embeds even length rings on hypercubes with small expansion and recovery cost. It is shown that the average expansion for the proposed scheme is 1.58, and the average number of …
Formation Of Clusters And Resolution Of Ordinal Attributes In Id3 Classification Trees, Chaman Sabharwal, Keith R. Hacke, Daniel C. St. Clair
Formation Of Clusters And Resolution Of Ordinal Attributes In Id3 Classification Trees, Chaman Sabharwal, Keith R. Hacke, Daniel C. St. Clair
Computer Science Faculty Research & Creative Works
Many learning systems have been designed to construct classification trees from a set of training examples. One of the most widely used approaches for constructing decision trees is the ID3 algorithm [Quinlan 1986]. Decision trees are ill-suited to handle attributes with ordinal values. Problems arise when a node representing an ordinal attribute has a branch for each value of the ordinal attribute in the training set. This is generally infeasible when the set of ordinal values is very large. Past approaches have sought to cluster large sets of ordinal values before the classification tree is constructed [Quinlan 1986; Lebowitz 1985; …
Parallel Error Tolerance Scheme Based On The Hill Climbing Nature Of Simulated Annealing, Bruce M. Mcmillin, Chul-Eui Hong
Parallel Error Tolerance Scheme Based On The Hill Climbing Nature Of Simulated Annealing, Bruce M. Mcmillin, Chul-Eui Hong
Computer Science Faculty Research & Creative Works
In parallelizing simulated annealing in a multicomputer, maintaining the global state S involves explicit message traffic and is a critical performance bottleneck. One way to mitigate this bottleneck is to amortize the overhead of these state updates over as many parallel state changes as possible. Using this technique introduces errors in the calculated cost C(S) of a particular state S used by the annealing process. Analytically derived bounds are placed on this error in order to assure convergence to the correct result. The resulting parallel simulated annealing algorithm dynamically changes the frequency of global updates as a function of the …
Experimentation With Proof Methods For Non-Horn Sets, Christopher J. Merz, Ralph W. Wilkerson
Experimentation With Proof Methods For Non-Horn Sets, Christopher J. Merz, Ralph W. Wilkerson
Computer Science Faculty Research & Creative Works
Two Resolution Proof Strategies Developed by Peterson Are Implemented by Modifying Otter, an Existing Automated Theorem Prover. the Methods, Lock-T Refutation and LNL-T Refutation, Are Generalizations of Unit Refutation and Input Resolution, Respectively, to Non-Horn Sets and Represent Independent, Equivalent but Opposite Ways of Searching. the Algorithms Used Are based on a Corrected Version of the Foundational Work. the Strategies Have Been Tested on Various Non-Horn Challenge Problems from the Tarskian Geometry and the Non-Obvious Problem, with the Results Being in Some Cases Quite Favorable When Compared to Other Resolution Techniques.
Proving Functionally Difficult Problems Through Model Generation, Richard Rankin, Ralph W. Wilkerson
Proving Functionally Difficult Problems Through Model Generation, Richard Rankin, Ralph W. Wilkerson
Computer Science Faculty Research & Creative Works
Satchmo [MA88] is a Theorem Prover Implemented in Prolog Which Attempts to Provide Satisfiability Checking through Model Generation. This Paper Gives a Brief Introduction to SATCHMO and Reports Extensions to the Original Work Which Allow SATCHMO to Solve Problems Previously Considered to Be Finitely Unprovable within the SATCHMO System. the Specific Problems Are from [PE86, MO85, LU85] and Were Designed to Convert Simple Propositional Logic Problems into Functionally Difficult First Order Problems. Although the Benefits of using the SATCHMO System Are Many, the Fact that It Could Not Offer Proofs for a Set of Problems Provable in Other Systems is …
Fault-Tolerant Concurrent Branch And Bound Algorithms Derived From Program Verification, Hanan Lutfiyya, Aggie Sun, Bruce M. Mcmillin
Fault-Tolerant Concurrent Branch And Bound Algorithms Derived From Program Verification, Hanan Lutfiyya, Aggie Sun, Bruce M. Mcmillin
Computer Science Faculty Research & Creative Works
An important aspect which is often overlooked in software design of distributed environments is that of fault tolerance. Many methodologies in the past have attempted to provide fault tolerance efficiently but have never been successful at eliminating explicit time and space redundancy. One approach for providing fault tolerance is through examining the behavior and properties of the application and deriving executable assertions that detect faults. Our work focuses on transforming the assertions of a verification proof of a program to executable assertions. These executable assertions may be embedded in the program to create a fault-tolerant program. It is also shown …
Semi-Supervised Adaptive Resonance Theory (Smart2), Christopher J. Merz, William E. Bond, Daniel C. St. Clair
Semi-Supervised Adaptive Resonance Theory (Smart2), Christopher J. Merz, William E. Bond, Daniel C. St. Clair
Computer Science Faculty Research & Creative Works
Adaptive resonance theory (ART) algorithms represent a class of neural network architectures which self-organize stable recognition categories in response to arbitrary sequences of input patterns. The authors discuss incorporation of supervision into one of these architectures, ART2. Results of numerical experiments indicate that this new semi-supervised version of ART2 (SMART2) outperformed ART for classification problems. The results and analysis of runs on several data sets by SMART2, ART2, and backpropagation are analyzed. The test accuracy of SMART2 was similar to that of backpropagation. However, SMART2 network structures are easier to interpret than the corresponding structures produced by backpropagation.
Constrained Completion: Theory, Implementation, And Results, Daniel Patrick Murphy
Constrained Completion: Theory, Implementation, And Results, Daniel Patrick Murphy
Doctoral Dissertations
"The Knuth-Bendix completion procedure produces complete sets of reductions but can not handle certain rewrite rules such as commutativity. In order to handle such theories, completion procedure were created to find complete sets of reductions modulo an equational theory. The major problem with this method is that it requires a specialized unification algorithm for the equational theory. Although this method works well when such an algorithm exists, these algorithms are not always available and thus alternative methods are needed to attack problems. A way of doing this is to use a completion procedure which finds complete sets of constrained reductions. …
Composite Stock Cutting Through Simulated Annealing, Hanan Lutfiyya, Bruce M. Mcmillin, Pipatpong Poshyanonda, Cihan H. Dagli
Composite Stock Cutting Through Simulated Annealing, Hanan Lutfiyya, Bruce M. Mcmillin, Pipatpong Poshyanonda, Cihan H. Dagli
Computer Science Faculty Research & Creative Works
This paper explores the use of Simulated Annealing as an optimization technique for the problem of Composite Material Stock Cutting. The shapes are not constrained to be convex polygons or even regular shapes. However, due to the composite nature of the material, the orientation of the shapes on the stock is restricted. For placements of various shapes, we show how to determine a cost function, annealing parameters and performance. © 1992.
An Lr(L) Testing Algorithm, Thomas J. Ssager
An Lr(L) Testing Algorithm, Thomas J. Ssager
Computer Science Technical Reports
A grammar is LR{1} if it can be parsed deterministically from left to right while looking ahead no more than one symbol. Because of the difficulty in generating full LR{l) parsers, many parser generators such as YACC limit themselves to LALR(1} grammars which are a subset of the LR{l) grammars.
Unlike other algorithms in the literature for testing whether a grammar is LR{l), the algorithm presented here uses only the characteristic finite state machine and other structures necessary for creating an LALR{l) parser. Thus, if a parser generator finds that a grammar is not LALR{l), with little additional work the …
The Minlrl Algorithm For Generating Small Lr(L) Parsers, Thomas J. Sager
The Minlrl Algorithm For Generating Small Lr(L) Parsers, Thomas J. Sager
Computer Science Technical Reports
The MINLRl algorithm for finding minimal deterministic parsers for LR(1) grammars is presented. MINLRl also detects whether a grammar is LR(l) with little more work than building the grammar's LALR(l) parser. MINLRl starts by building the characteristic finite state machine, CFSM, for the input grammar and then checks for LR(l)ness. If the input grammar is LR(l), MINLRl transforms the CFSM into a minimal LR(l) parser by creating extra copies of certain states of the CFSM as necessary. The complexity of the algorithm is O(n3l2v2) where n is the number of states in the parser, …
Formal Generation Of Executable Assertions For A Fault-Tolerant Parallel Matrix Relaxation, Hanan Lutfiyya, Bruce M. Mcmillin
Formal Generation Of Executable Assertions For A Fault-Tolerant Parallel Matrix Relaxation, Hanan Lutfiyya, Bruce M. Mcmillin
Computer Science Technical Reports
No abstract provided.
Composite Stock Cutting Through Simulated Annealing, Pipatpong Poshyanonda, Cihan H. Dagli
Composite Stock Cutting Through Simulated Annealing, Pipatpong Poshyanonda, Cihan H. Dagli
Computer Science Technical Reports
This paper explores the use of Simulated Annealing as an optimization technique for the problem Composite Material Stock Cutting. The shapes are not constrained to be convex polygons or even regular shapes. However, due to the composite nature of the material, the orientation of the shapes on the stock is restricted. For placements of various shapes, we show how to determine a cost function, annealing parameters, and performance.
Fault-Tolerant Parallel Matrix Multiplication With One Iteration Fault Detection Latency, Chul-Eui Hong, Bruce M. Mcmillin
Fault-Tolerant Parallel Matrix Multiplication With One Iteration Fault Detection Latency, Chul-Eui Hong, Bruce M. Mcmillin
Computer Science Technical Reports
The checksum technique is a low cost method to detect errors in matrix operations performed by processor arrays. The fault detection of this method is done only at problem termination, so this method is not an effective fault tolerance technique for large scale matrix multiplication.
This paper presents a new algorithm, the ID algorithm, which minimizes the fault-detection latency, In the ID algorithm, a fault is detected as soon a5 the fault occurs instead of at problem termination. For 112 processors, the fault-latency time of the ID algorithm is l/11 of that of checksum algorithm with a run-time penalty of …
Composite Stock Cutting Through Simulated Annealing, Pipatpong Poshyanonda, Cihan H. Dagli
Composite Stock Cutting Through Simulated Annealing, Pipatpong Poshyanonda, Cihan H. Dagli
Computer Science Technical Reports
This paper explores the use of Simulated Annealing as an optimization technique for the problem Composite Material Stock Cutting. The shapes are not constrained to be convex polygons or even regular shapes. However, due to the composite nature of the material, the orientation of the shapes on the stock is restricted. For placements of various shapes, we show how to determine a cost function, annealing parameters, and performance.
Fault-Tolerant Parallel Matrix Multiplication With One Iteration Fault Detection Latency, Chul-Eui Hong, Bruce M. Mcmillin
Fault-Tolerant Parallel Matrix Multiplication With One Iteration Fault Detection Latency, Chul-Eui Hong, Bruce M. Mcmillin
Computer Science Technical Reports
The checksum technique is a low cost method to detect errors in matrix operations performed by processor arrays. The fault detection of this method is done only at problem termination, so this method is not an effective fault tolerance technique for large scale matrix multiplication.
This paper presents a new algorithm, the ID algorithm, which minimizes the fault-detection latency, In the ID algorithm, a fault is detected as soon a5 the fault occurs instead of at problem termination. For 112 processors, the fault-latency time of the ID algorithm is l/11 of that of checksum algorithm with a run-time penalty of …
Formal Methods Of Real-Time Systems, Su-Mei Tsai, Bruce M. Mcmillin
Formal Methods Of Real-Time Systems, Su-Mei Tsai, Bruce M. Mcmillin
Computer Science Technical Reports
Formal aid in specification and verification techniques have become an accepted approach to achieving reliable software for life-critical real-time systems, in which testing may be impossible or too dangerous, since the real inputs to the systems come from the real world. Modelling, assertion languages, and proof systems are three major components that are employed to accomplish the confidence of safe real-time environments. This paper examines these currently available techniques that are used for safety analysis of real-time systems.
Application-Oriented Fault-Tolerant Parallel Branch & Bound, Aggie Sun, Bruce M. Mcmillin
Application-Oriented Fault-Tolerant Parallel Branch & Bound, Aggie Sun, Bruce M. Mcmillin
Computer Science Technical Reports
An important aspect which is often overlooked in the software design cycle is the question of reliability. Many methodologies in the past have attempted to provide reliability efficiently but have never been successful at eliminating explicit time and space redundancy. The approach taken here is based on the Application-Oriented Fault Tolerance Paradigm which provides reliability by examining the behavior and properties of the application. This paper will demonstrate how fault detecting constraints are developed and incorporated using the Application-Oriented Fault Tolerance paradigm for the class of Branch and Bound algorithms. Branch and bound algorithms are a type of combinatorial search …
Multi Cast Routing In Unreliable Networks, Martina Schollmeyer, Bruce M. Mcmillin
Multi Cast Routing In Unreliable Networks, Martina Schollmeyer, Bruce M. Mcmillin
Computer Science Technical Reports
The efficient routing of messages in a multicomputer interconnection network is the key to the performance of such a network. Multicast communication refers to the delivery of a message from a source node to several destination nodes. Although multicast is highly desirable for many applications, it is not directly supported in most multicomputer architectures. This paper examines existing algorithms for multicast routing in multicomputer networks and groups them into a number of categories such as multicast trees, multicast paths, multicast stars, etc. These algorithms are evaluated in terms of deadlock handling, adaptability and suitability for wormhole routing. Wormhole routing is …
Formal Generation Of Executable Assertions For A Fault-Tolerant Parallel Bitonic Sort, Hanan Lutfiyya, Bruce M. Mcmillin
Formal Generation Of Executable Assertions For A Fault-Tolerant Parallel Bitonic Sort, Hanan Lutfiyya, Bruce M. Mcmillin
Computer Science Technical Reports
No abstract provided.
Fast Symmetric Graph Drawing: Theory And Realization, R. T. Pacheco, J. B. Manning
Fast Symmetric Graph Drawing: Theory And Realization, R. T. Pacheco, J. B. Manning
Computer Science Technical Reports
This thesis explores the computational techniques necessary to efficiently realize certain optimal algorithms for the production of drawings which exhibit maximum axial and rotational symmetries of abstract graphs.
The problem of geometric symmetry detection for general graphs has been shown to be NP-complete. However, optimal algorithms have recently been established for the detection of symmetry in trees, outerplanar graphs, and embedded planar graphs. This thesis focuses on the utilization of these algorithms to efficiently produce maximally symmetric drawings of graphs from the classes of symmetric trees and outerplanar graphs.
The construction of symmetric tree drawings is presented first. Following a …
Smili-Visualization Of Asynchronous Massively Parallel Programs, Rashi Khanna, Bruce M. Mcmillin
Smili-Visualization Of Asynchronous Massively Parallel Programs, Rashi Khanna, Bruce M. Mcmillin
Computer Science Technical Reports
A visualization model has been developed to analyse the performance of a massively parallel algorithm. Most visualization tools that have been developed so far for performance analysis are based generally on individual processor information and communication patterns (eg. processor load, message traffic etc.). These tools, however, are inadequate for massively parallel computations. It is difficult to comprehend the visual information for many processors. The model, SMil...l (Scientific visualization in Multicomputing for Interpretation of Large amounts of Information), addresses this problem by using abstract representations to attain a composite picture which gives better insight to the behavior of the algorithm. Chernoff's …
Comparison Of Three Axiomatic Systems For Csp, Hanan Lutfiyya, Bruce M. Mcmillin
Comparison Of Three Axiomatic Systems For Csp, Hanan Lutfiyya, Bruce M. Mcmillin
Computer Science Technical Reports
Currently software engineering practices use relatively few formal methods. However, formal methods can be used to find errors earlier in the software cycle and hence reduce software cost. One useful formal method is program verification. The axiomatic approach to program verification uses assertions to characterize properties of program variables and relationships between them at various stages of program execution. In order to verify these assertions, axioms or inference rules are needed for each statement as well as some statement-independent inference rules. The message passing and nondeterminism of a distributed programming language present special difficulties. This paper examines and compares three …