An Interactive Program Verification System
Abstract
This paper is an initial progress report on the development of an interactive system for verifying that computer programs meet given formal specifications. The system is based on the conventional inductive assertion method: given a program and its specifications, the object is to generate the verification conditions, simplify them, and prove what remains. This system addresses two aspects of software improvement of extreme importance to the military: increase in the quality of software and decrease in the cost of producing high-quality software. A general description is given of the overall design philosophy, structure, and functional components of the system, and a simple sorting program is used to illustrate both the behavior of major system components and the type of user interaction the system provides.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1974
- Accession Number
- ADA002279
Entities
People
- Donald I. Good
- Ralph L. London
- W. W. Bledsoe
Organizations
- University of Southern California