Browse Prior Art Database

Program Verification in the 1980s: Problems, Perspectives, and Opportunities

IP.com Disclosure Number: IPCOM000128656D
Original Publication Date: 1978-Dec-31
Included in the Prior Art Database: 2005-Sep-16
Document File: 20 page(s) / 71K

Publishing Venue

Software Patent Institute

Related People

Susan L. Gerhart: AUTHOR [+3]

Abstract

Properties of programs can be mathematically proved. This report concerns the use of such mathematical proofs as a means of verifying that programs satisfy their specifications and other expectations of proper behavior. Moreover, the theory by means of which programs are proved can be used in the formal reasoning Itr`rood t0 CAflStrtlct and maintain programs. The primary current needs are: (1) Vxhansion of the theory to encompass more aspects of program correctness, (2) evolution of the theory's mathematical content and form to make it more effective in vr*rifyin~; prof;rams, (;i) experimentation with new and current techniques for utinp; the ihr*ory in verification and construction, (4) development of.' human. knowledge and skills to fulfill human roles of specifying, and guiding program proofs, (,y technological support to take over mechanical parts of the proofs and follow human guidance. in elaborating them.

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

Page 1 of 20

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Program Verification in the 1980s: Problems, Perspectives, and Opportunities

Susan L. Gerhart

INFORMATION SCIENCES INSTITUTE

46 76 Admiralty TGay/Mariaaael KeylCalifosrria 90291 UNIVERSITY OF SOUTHERN CALIFORNIA (213) 822-1 S 11

THIS RESEARCH IS SUPPORTED BY THE ADVANCED RESEARCH PROJECTS AGENCY UNDER CONTRACT NO. DAHC15 72 C 0308, ARPA ORDER NO. 2223. VIEWS AND CONCLUSIONS CONTAINED IN THIS STUDY ARE THE AUTHOR'S AND SHOULD NOT BE INTERPRETED AS REPRESENTING THE OFFICIAL OPINION OR POLICY OF ARPA, THE U.S. GOVERNMENT OR ANY OTHER PERSON OR AGENCY CONNECTED WITH THEM.

THIS DOCUMENT APPROVED FOR PUBLIC RELEASE AND SALE: DISTRIBUTION IS UNLIMITED.

CONTENTS

Acknowledgments iv Abstract v i. Introduction 1

2. Current Problems, Obstacles, and Steps to Overcome Them 4

3. Needed Advances and Breakthroughs 14

et. Effects of PV Sol ution/Breaktlarouhs on Computing an the 1980s 16

Appendix 19

References 26

ACKNOWLEDGMENTS

The ISI Prol;ram Verification group has been very helpful in formulating the problems and needed breakthroughs discussed in this paper and in criticizing the final version. However, any distortions or omissions are my responsibility. I would also like to thank Brian Randell for sending me the Turing material.

ABSTRACT

University of Southern California Page 1 Dec 31, 1978

Page 2 of 20

Program Verification in the 1980s: Problems, Perspectives, and Opportunities

Properties of programs can be mathematically proved. This report concerns the use of such mathematical proofs as a means of verifying that programs satisfy their specifications and other expectations of proper behavior. Moreover, the theory by means of which programs are proved can be used in the formal reasoning Itr`rood t0 CAflStrtlct and maintain programs. The primary current needs are: (1) Vxhansion of the theory to encompass more aspects of program correctness, (2) evolution of the theory's mathematical content and form to make it more effective in vr*rifyin~; prof;rams, (;i) experimentation with new and current techniques for utinp; the ihr*ory in verification and construction, (4) development of.' human. knowledge and skills to fulfill human roles of specifying, and guiding program proofs, (,y technological support to take over mechanical parts of the proofs and follow human guidance. in elaborating them.

7'hc* nc*c*dc*

I. INTRODUCTION

Before looking into the future of program verification it is worth reconsidering, Turing's advice of nearly three decades ago, especially regarding the weaknesses of the two extreme positions. The theoretical approach must deal with the fact that very few mathematicians ever carry out a proof down to the last detail of axioms and rules of inference because the process is simply too exhausting for both writer and reader and is still prone to error. (Unlike Turing, we can envision the possibility of mechanizing much of the detailed proof effort, although this is ono of...