Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

A SURVEYOF PROGRAM PROOF TECHNOLOGY

IP.com Disclosure Number: IPCOM000128151D
Original Publication Date: 1978-Dec-31
Included in the Prior Art Database: 2005-Sep-15
Document File: 21 page(s) / 74K

Publishing Venue

Software Patent Institute

Related People

JACOB T. SCHWARTZ: AUTHOR [+3]

Abstract

Several government, agencies,, including DOD., NASAy and DOE use computers to control equir-ment, whose malfunction or failure can have catar:-'Crophic consequences. Within XASA,, the failure of a program controlling an experiment which has been transported at enormous expense to an outer planet is surely unacceptable. DOE must find the possibility of failure in a program controlling a large nuclear reactor even more alarming. DOD cannot accept the possibility that a supposedly secure ccmmmications system should be compromised by a program failure which gives an unauthorised user access to supposedly protected information within a distributed system. in some cases., program failures of this sort are officially discountenanced in regulations issued by authoritative bodies. The FAA., for example., has d that programs used to control aircraft landings be certified as having very small error probability. It is not hard to predict that the probability of failure in critical control programs., e.g. reactor control programs,, may even become matters of direct courtroan dispute. The problem of rigorous certification of programs is therefore unescapable. The problem of proving programs correct has existed since the first computers were constructed, and has steadily grown more pressing as programs have increased in complexity. The large number of papers (close to 800) that have been written in this area have established program verification as a recognised subfield of computer science. But in spite of all this work., a truly practical program verification technology,has been slow to developy and is still not at hazd. Indeed., the history to date of program verification makes one key fact quite clear: The problem of verifying large programs rigorously is a very difficult one, and its solution will imply significant changes in current programing technology. This paper will review vaxious salient aspects of the verification problem., assess progress to date, point out major difficulties which remain, and attempt to project future directions of progress.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 5% of the total text.

Page 1 of 21

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

A SURVEYOF PROGRAM PROOF TECHNOLOGY

BY JACOB T. SCHWARTZ

SEPTEMBER 1978 REPORT NO. 001

This survey was written on contract to the Office of Naval Research. A Survey of Program Proof Technology

J. T. Schwaxtz

Computer Science Department Courant :Enstitute of Mathematical Sciences New York University

.1. Why-is it necessary to prove programe correct?

.Several government, agencies,, including DOD., NASAy and DOE use computers to control equir-ment, whose malfunction or failure can have catar:-'Crophic consequences. Within XASA,, the failure of a program controlling an experiment which has been transported at enormous expense to an outer planet is surely unacceptable. DOE must find the possibility of failure in a program controlling a large nuclear reactor even more alarming. DOD cannot accept the possibility that a supposedly secure ccmmmications system should be compromised by a program failure which gives an unauthorised user access to supposedly protected information within a distributed system. in some cases., program failures of this sort are officially discountenanced in regulations issued by authoritative bodies. The FAA., for example., has d that programs used to control aircraft landings be certified as having very small error probability. It is not hard to predict that the probability of failure in critical control programs., e.g. reactor control programs,, may even become matters of direct courtroan dispute. The problem of rigorous certification of programs is therefore unescapable. The problem of proving programs correct has existed since the first computers were constructed, and has steadily grown more pressing as programs have increased in complexity. The large number of papers (close to 800) that have been written in this area have established program verification as a recognised subfield of computer science. But in spite of all this work., a truly practical program verification technology,has been slow to developy and is still not at hazd. Indeed., the history to date of program verification makes one key fact quite clear: The problem of verifying large programs rigorously is a very difficult one, and its solution will imply significant changes in current programing technology. This paper will review vaxious salient aspects of the verification problem., assess progress to date, point out major difficulties which remain, and attempt to project future directions of progress.

2. How is it possible to prove programs correct?

To prove programs correct, one can begin by giving formal mathematical defini.tion to the notions. 'program.' and 'program execution'. Essentially, these mathematical definitions merely formalise the basic facts concerning programs and their meaning that one would present in a

Northwestern University Page 1 Dec 31, 1978

Page 2 of 21

A SURVEYOF PROGRAM PROOF TECHNOLOGY

first course on programmi . A 'program' can be defined formally as a s...