A New Verification Strategy for Iterative Programs.

Abstract

A new verification strategy for interative programs is described. The technique is based on the idea of applying a correctness/incorrectness preserving transformation to the program to be verified. The transformation is performed in such a way that the new program is substantially easier to verify than the original. Examples which illustrate the use of the technique are presented. The method is compared and contrasted with subgoal induction and the inductive assertion technique. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1981
Accession Number
ADA114000

Entities

People

  • Douglas D. Dunlop
  • Victor Basili

Organizations

  • University of Maryland

Tags

DTIC Thesaurus Topics

  • Air Force
  • Boundaries
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Engineering
  • Hypotheses
  • Identities
  • Iterations
  • Maryland
  • Notation
  • Software Development
  • Specifications
  • Standards
  • Universities
  • Verification

Readers

  • Artificial Intelligence
  • Computational Modeling and Simulation
  • Finite Element Method (FEM) for solving Partial Differential Equations (PDEs)