Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
Date: 	Mon, 27 Nov 1995 10:13:44 -0800
From: homeier@uniblab.aero.org (Peter Homeier)
Message-Id: <9511271813.AA12645@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 am happy to announce the availability of my doctoral dissertation,
with my recent graduation from UCLA in June, 1995.

The dissertation is entitled,

"Trustworthy Tools for Trustworthy Programs:
 A Mechanically Verified Verification Condition Generator
 for the Total Correctness of Procedures".

This may be obtained by anonymous ftp from the internet site
ftp.cs.ucla.edu, in directory /pub/homeier/dissertation.
There is both a .ps and a .dvi file, and both have been compressed
using gzip.  The .ps file contains only 300dpi fonts, so if you wish 
to print at a different resolution, you may wish to use the .dvi file.

These two files may also be obtained through the World Wide Web at
URL's

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

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. 

(Tom: thanks for the suggestion!)

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