Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Mon, 18 Sep 1995 15:46:07 +0200 (METDST)
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
To: hol mailing list <info-hol@leopard.cs.byu.edu>
Subject: thesis on design of distr. algorithms with HOL available
Message-Id: <Pine.HPP.3.91.950918153821.432c-100000@muddy.cs.ruu.nl>
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII

Dear HOL users,

In October I will be defending my Ph.D thesis at Utrecht University, the
Netherlands.

Below I will give a short discription of my thesis, which I'm sure
some of you will find interesting. Since I only have a limited number
of printed copies, I will simply put the postscript version of my
thesis in the following www address:

   http://www.cs.ruu.nl/~wishnu/start_jade.html

Feel free to print a copy if it interests you. All libraries that I
wrote during my research will also be made available as soon as I have
it set-up in our ftp archieves.

The thesis is motivated by the question: how to mechanically verify a
distributed algorithm? My experience pointed out that verifying such
an algorithm requires lots of hand-guided proofs. In various papers
people have investigated how to embed various programming logics in
HOL. For a practical use of HOL --especially in cases where lots of
hand-guided proofs are required-- I think we also need to investigate
how various design strategies can be expressed in HOL.

The interesting point of my thesis are (in my opinion):

      - the development of a methodology for reasoning about
        self stabilising distributed algorithms
      - the expression of proof rules for this as an extension of 
        the UNITY logic
      - the application of this to the design of a 
        non-trival distributed algorithm
      - the complete verification of the corrected UNITY logic
        and the distribuetd algorithm in HOL
        (amounting to about 750 kb of HOL code)
      - as a side effect many mathematical facts about partial orders etc.
        had to be developed, and have in this way become available for others

If you have any qustions I would be very happy to answer them, but
since I will be leaving the department (and most likely the
Netherlands) soon after the defense of my thesis, and I do not know
what my next job will be like --not even know if I will have internet
access-- I am asking you kindly to pose those questions as soon as
possible.

Wishnu Prasetya
Dept. of Comp. Science
Utrecht University
the Netherlands
wishnu@cs.ruu.nl

---------------------------------

PS: For Carlos (?) from Mexico, I tried to reach you, even trying to
do so via Phill but I never got your response. I still want to send
you a copy of my thesis if you just can give me your regular mail
address.