Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Sat, 19 Mar 1994 08:48:55 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA13219;
          Sat, 19 Mar 1994 01:32:21 -0700
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from Maui.CS.UCLA.EDU by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA13215;
          Sat, 19 Mar 1994 01:32:18 -0700
Received: from LocalHost.cs.ucla.edu by maui.cs.ucla.edu (Sendmail 4.1/3.25) 
          id AA17819; Sat, 19 Mar 94 00:32:24 PST
Message-Id: <9403190832.AA17819@maui.cs.ucla.edu>
To: info-hol@leopard.cs.byu.edu
Subject: Two papers available via anonymous FTP
Date: Sat, 19 Mar 94 00:32:23 PST
From: chou@cs.ucla.edu

The following two papers are now available via anonymous FTP at:

    ftp.cs.ucla.edu:/pub/chou

Their names are [1] dsum.ps and [2] graph.ps
All comments will be appreciated.

- Ching Tsun


[1] Ching-Tsun Chou,
    "Mechanical Verification of Distributed Algorithms in Higher-Order Logic"
    

    ABSTRACT:
    Distributed algorithms have to work correctly
    in the face of total asynchrony.
    The only way to verify the correctness of a distributed algorithm
    with a high degree of confidence is to construct a correctness proof
    that is so formal and rigorous as to be checkable by a machine.
    The chief aim of this paper is to show,
    via a simple but typical example,
    how such proofs can be constructed and checked
    using the mechanical theorem proving system HOL.
    The secondary aim of this paper is to demonstrate
    an event-based methodology for verifying distributed algorithms,
    in which a distributed algorithm is verified in four steps:
    (a) we introduce an {\em event algorithm\/}
    that is an operational representation of
    the causal patterns of events of the distributed algorithm,
    (b) we derive properties of the event algorithm
    using event-based reasoning,
    (c) we show that the event algorithm {\em simulates\/}
    the distributed algorithm, and
    (d) we {\em translate\/} the properties of the event algorithm
    into those of the distributed algorithm via the simulation relation.
    The goal is to perform as much reasoning as possible
    in terms of the event algorithm, which is more abstract and
    easier to reason about than the distributed algorithm.
    The example we use to illustrate these ideas
    is the verification of $\Dsum$,
    which is a simple distributed summation algorithm for trees.
    A companion paper [2] describes the formal graph theory
    needed to reason about distributed algorithms like $\Dsum$.

[2] Ching-Tsun Chou,
    "A Formal Theory of Undirected Graphs in Higher-Order Logic"
    

    ABSTRACT:
    This paper describes a formal theory of {\em undirected\/} graphs
    in higher-order logic
    developed using the mechanical theorem proving system HOL.
    It formalizes and proves theorems about such notions as
    the empty graph, single-node graphs, finite graphs, subgraphs,
    adjacency relations, walks, paths, cycles, bridges, reachability,
    connectedness, acyclicity, trees,
    trees oriented with respect to roots,
    oriented trees viewed as family trees,
    top-down and bottom-up inductions in family trees,
    distributing associative and commutative operations with identities
    recursively over subtrees of family trees,
    and joining two disjoint subgraphs via a link in a graph.
    The main contribution of this work lies in 

    the precise formalization of these graph-theoretic notions and
    the rigorous derivation of their properties in higher-order logic.
    This is difficult because there is little tradition of formalization
    in graph theory due to the concreteness of graphs.
    A companion paper [1] describes 

    the application of this formal graph theory
    to the mechanical verification of distributed algorithms.