Trustworthy Tools
Dissertation
Home | About Us | Projects | HOL-Omega | Publications | Dissertation | Divine Support

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

by Peter Vincent Homeier

Abstract

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.

This dissertation was only accomplished by God's grace. Soli Deo Gloria. (To God alone be the glory.)

Associated software

This dissertation has been implemented in a package called Sunrise for the Higher Order Logic theorem prover.

Download a copy of the dissertation.

The dissertation may be downloaded either in one file, or one chapter at a time. Both postscript and PDF versions are provided.

525,606 bytes, 341 pages
859,260 bytes, 341 pages
gzipped tar archive,
containing DVI file and all assocated EPS images
386,040 bytes, 341 pages

Postscript and PDF files
Chapter Title
Contents
Preliminary Pages
Title page, Signature page, Dedication, Table of Contents, List of Figures, List of Tables, Acknowledgments, Vita, Publications, Abstract
 

Part I:

Background
Chapter 1:
Introduction
Introduces and motivates the need for program correctness, and introduces the concept of verification condition generators.
Chapter 2:
Underlying Technologies
Describes the foundational technologies that underlie this work, such as structural operational semantics and Floyd/Hoare rules.
Chapter 3:
Survey of Previous Research
A survey of previous research on verification condition generators, and in particular, methods to prove the total correctness of procedures.
Chapter 4:
Organization of Dissertation
Gives the overall organization of the dissertation, and description of each chapter.
 

Part II:

Results
Chapter 5:
Sunrise
Defines the syntax and semantics of the Sunrise programming language and assertion language.
Chapter 6:
Program Logics
Presents the five program logics, with their fourteen correctness specifications, that can be used to prove Sunrise programs totally correct.
Chapter 7:
Verification Condition Generator
The heart of this work. Defines a verification condition generator for the Sunrise system, and also presents theorems that verify it.
Chapter 8:
Example Runs
Takes this VCG and applies it to several examples, with transcripts.
Chapter 9:
Source Code
Describes the source code of the Sunrise system and where it may be found.
 

Part III:

Tour of Interesting Aspects
Chapter 10:
Partial Correctness
Describes various aspects of the system relating to partial correctness, including variants, substitution, translation, well-formedness, and semantic stages.
Chapter 11:
Total Correctness
Describes the proof of termination of mutually recursive procedures and programs.
 

Part IV:

Conclusions
Chapter 12:
Significance
Our sense of this work's significance.
Chapter 13:
Ease of Use
Examines the question of ease of use for Sunrise.
Chapter 14:
Future Research
Gives an outline of our plans for future research in this area.
Chapter 15:
Conclusions and References
Presents our conclusions.
Includes the list of references.

Making formal methods into normal methods.