Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Date: Sat, 2 Dec 1995 16:36:17 -0800
From: homeier@uniblab.aero.org (Peter Homeier)
Message-Id: <9512030036.AA16486@baggins.itd>
To: info-hol@cs.byu.edu
Subject: Ph.D. Dissertation now available
Cc: dmartin@cs.ucla.edu, stott@cs.ucla.edu, rajive@cs.ucla.edu, 
    dam@math.cs.ucla, tfm@dcs.gla.ac.uk, homeier@cs.ucla.edu

I have revised somewhat the form of my dissertation as available on 
the Internet, in order to make it more accessable.

The easiest way is through a new Web Ph.D. page, at

http://www.cs.ucla.edu/csd-grads-gs2/homeier/html/phd.html

As before, the compressed postscript is in

ftp://ftp.cs.ucla.edu/pub/homeier/dissertation/diss.ps.gz

There is now a tar archive of the dvi file and associated EPS images
together in one package, in

ftp://ftp.cs.ucla.edu/pub/homeier/dissertation/diss.dvi.tar.gz

If people would like to look at individual chapters, they are available
one at a time in

ftp://ftp.cs.ucla.edu/pub/homeier/dissertation/chapters/

Here is the abstract.


                        Abstract of the Dissertation 

As an alternative to testing, formal proofs of a program's correctness may 
be constructed.  The application of these techniques has been limited by the 
difficulty of constructing the required proofs by hand.  The task of proving 
a program correct can be simplified and eased by a tool called a 
Verification Condition Generator (VCG).  The VCG processes programs written 
in the specified language, and produces as its result a set of lemmas called 
verification conditions, as the remainder left for the programmer to prove.  
The truth of these is intended to imply the correctness of the program.  
However, most VCGs that have been written have not themselves been verified, 
making that support unreliable. 

We have written a VCG and verified its soundness, proving that if the 
verification conditions produced are true, then the original program is 
totally correct.  This proof is conducted within and checked by the Higher 
Order Logic (HOL) mechanical proof checker, ensuring its complete soundness. 
The resulting verified VCG provides an effective means for proving programs 
totally correct with complete security. 

The programming language studied contains two areas of special interest, 
expressions with side effects, and mutually recursive procedures, with 
global variables and variable and value parameters.  As part of this work, 
we provide five program logics which together provide an axiomatic semantics
for total correctness. Of the five program logics, three are fundamental 
inventions in this dissertation.  These new program logics are used to 
verify the correctness of expressions, the progress achieved between 
recursive calls of the same procedure, and the termination of procedures.  
All of these logics are mechanically proven within the HOL system to be 
sound with respect to the formal semantics of the language. 

The most novel contribution of this dissertation is the discovery of a new 
method for proving the termination of programs with mutually recursive 
procedures, which is both more general and easier to use than prior 
proposals.  In addition, VCG automation is naturally supported.  This method
analyzes the structure of the procedure call graph, generating verification 
conditions based on the cycles found. 

                              End of Abstract 


This dissertation was only accomplished by God's grace.  Soli Deo Gloria. 

Peter Homeier
homeier@cs.ucla.edu
http://www.cs.ucla.edu/csd-grads-gs2/homeier/html/