Accession Number : AD0699248

Title :   A PROGRAM VERIFIER.

Descriptive Note : Doctoral thesis,

Corporate Author : CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

Personal Author(s) : King,James C.

Report Date : SEP 1969

Pagination or Media Count : 262

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)

Descriptors :   (*COMPUTER PROGRAMMING, CORRECTIONS), (*COMPILERS, CORRECTIONS), PROGRAMMING LANGUAGES, CONTROL SEQUENCES, COMPUTER LOGIC, MACHINE TRANSLATION, THESES

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE