|
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.
| Description: |
Interim rept. 1 Jul 74-30 Jun 77 |
| Pages: |
126 |
| Report Date: |
NOV 1977 |
| Contract Number: |
F4462073C0068 |
| Report Number: |
A451050 |
Report Unavailable |
| This title is unavailable from Storming Media. We do not know when it might be available, if at all. We list the report on our site for bibliographic completeness, to help our users know what other work has been performed in this field. Please note that as with all titles on this site, we do not have contact information for any of the authors. Nor can we give any suggestions on how one might obtain this report. |
|
|
|
|
|
Keywords relating to this report:
Email This Abstract
