Algorithms for Program Verification.

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)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1982
Accession Number
ADA118570

Entities

People

  • Vaughan R. Pratt

Organizations

  • Massachusetts Institute of Technology

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Abstracts
  • Algorithms
  • Automata
  • Automatic
  • Classification
  • Computational Complexity
  • Computer Programming
  • Computer Science
  • Databases
  • Electrical Engineering
  • Engineering
  • Environment
  • Language
  • Programming Languages
  • Prosthetics
  • Security
  • Software Development

Readers

  • Computational Linguistics
  • Defense Acquisition Program Management
  • Technical Research and Report Writing.