A PROGRAM VERIFIER.
Abstract
The paper reports research toward developing a 'verifying compiler'. Such a compiler, as well as doing the standard translation of a program to machine executable form, attempts to prove that the program is 'correct'. In order to do this, a program must be annotated with propositions in a mathematical notation which define the 'correct' relations among the program variables. The verifying compiler then checks for consistency between the program and its propositions. The thesis presents the theoretical basis of the method and then describes a prototype verifier in detail. This verifier, running on an IBM 360, operates on programs written in a simple programming language for integer arithmetic. Many programs have been automatically verified by this program. These include a simple sort program, a program which examines a number for the property 'prime', and a rather subtle program which raises an integer to an integral power. The formal analysis of a program produced 'verification conditions' which must be proven to be theorems over integers. The verifier proves these theorems by using powerful formula simplification routines and specialized techniques for integer expressions. Ideas for improving this verifier and for building one which will operate on a more complicated programming language are also presented. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1969
- Accession Number
- AD0699248
Entities
People
- James C. King
Organizations
- Carnegie Mellon University