Automatic Program Verification III: A Methodology for Verifying Programs

Abstract

The paper investigates methods for applying an on-line interactive verification system designed to prove properties of PASCAL programs. The methodology is intended to provide techniques for developing a debugged and verified version starting from a program, that (a) is possibly unfinished in some respects, (b) may not satisfy the given specifications, e.g., may contain bugs, (c) may have incomplete documentation, (d) may be written in non-standard ways, e.g., may depend on user- defined data structures. The methodology involves (1) interactive application of a verification condition generator, an algebraic simplifier and a theorem-prover; (2) techniques for describing data structures, type constraints, and properties of programs and subprograms (i.e. lower level procedures); (3) the use of (abstract) data types in structuring programs and proofs.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Dec 01, 1974
Accession Number
ADA007563

Entities

People

  • David C. Luckham
  • Friedrich W. Henke

Organizations

  • Stanford University

Tags

Communities of Interest

  • Advanced Electronics
  • Autonomy
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Acceptability
  • Algorithms
  • Artificial Intelligence
  • Case Studies
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Debugging
  • Language
  • Notation
  • Programming Languages
  • Standards
  • Structured Programming
  • Test Methods
  • Universities

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computer Science.
  • Mathematical Modeling and Probability Theory.