Automatic Program Verification II: Verifying Programs by Algebraic and Logical Reduction

Abstract

Methods for verifying programs written in a higher level programming language are devised and implemented. The system can verify programs written in a subset of PASCAL, which may have data structures and control structures such as WHILE, REPEAT, FOR, PROCEDURE, FUNCTION and COROUTINE. The process of creation of verification conditions is an extension of the work done by Igarashi, London and Luckham which is based on the deductive theory by Hoare. Verification conditions are proved using specialized simplification and proof techniques, which consist of an arithmetic simplifier, equality replacement rules, fast algorithm for simplifying formulas using propositional truth value evaluation, and a depth first proof search process. The basis of deduction mechanism used in this prover is Gentzen-type formal system. Several sorting programs including Floyd's TREESORT3 and Hoare's FIND are verified. It is shown that the resulting array is not only well-ordered but also a permutation of the input array.

Open PDF

Document Details

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

Entities

People

  • Norihisa Suzuki

Organizations

  • Stanford University

Tags

Communities of Interest

  • Energy and Power Technologies
  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Algorithms
  • Arithmetic
  • Arrays (Data Structures)
  • Artificial Intelligence
  • Automatic
  • Computations
  • Computer Languages
  • Computer Programming
  • Computer Science
  • Language
  • Notation
  • Permutations
  • Programming Languages
  • Specifications
  • Standards
  • Test And Evaluation
  • Verification

Fields of Study

  • Engineering

Readers

  • Mathematical Modeling and Probability Theory.