Accession Number : ADA118570

Title :   Algorithms for Program Verification.

Descriptive Note : Final rept. 1 Jul 80-30 Jun 81,

Corporate Author : MASSACHUSETTS INST OF TECH CAMBRIDGE DEPT OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCE

Personal Author(s) : Pratt,Vaughan R

PDF Url : ADA118570

Report Date : May 1982

Pagination or Media Count : 8

Abstract : In the previous reporting period, July 1979 to June 1980, work was performed on (1) foundations for specifying automatic program verifiers (Pr1,Pr3), (2) decision methods for a large fragment of the basic logic of programs (Pr5), (3) implementation of a decision method for propositional dynamic logic, and (4) continued maintenance of MITVI (LP), a program verifier incorporating some of these ideas. In the current (and final) reporting period, the research emphasis shifted from the verification of sequential programs to that of dataflow programs. This week has led to new insights into the correspondence between functions and processes (Pr4,Pr7). It has also stimulated work on a new approach to user environments (Pr6). And it has raised, though not answered, problems concerning automated verification of dataflow programs. (Author)

Descriptors :   *Algorithms, *Computer program verification, *Data transmission systems, Computer logic, Decision making, Specifications, Semantics, Syntax, User needs

Subject Categories : Theoretical Mathematics
      Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE