A PROGRAM VERIFIER.
CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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
- Computer Programming and Software