The Semiautomatic Generation of Inductive Assertions for Proving Program Correctness.
Abstract
This interim report describes progress on a project aimed at solving a serious problem that has been encountered in attempts to make program correctness proving a practical technique for software verification. The principal problem addressed here is the difficulty of synthesizing so-called loop assertions in connection with the main method now under study for program proving. Several rather diverse approaches, some of them constituting such alternatives to the present technique, are considered here: transformation of programs into primitive recursive form before verification, the method of generator induction for proof of properties of complex data structures, the use of a hierarchical design methodology to structure programs so as to minimize the need for loop assertions, and methods related to subgoal induction and computational induction. The two latter methods were analyzed in detail and compared with the present approach to arrive at a better understanding of their mutual relationships.
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 1977
- Accession Number
- ADA050154
Entities
People
- Bernard Elspas
- J. Strother Moore
- Karl N. Levitt
- Lawrence Robinson
- Robert S. Boyer
Organizations
- SRI International