Automatic Program Verification 1: A Logical Basis and Its Implementation

Abstract

Defining the semantics of programming languages by axioms and rules of inference yields a deduction system within which proofs may be given that programs satisfy specifications. The deduction system herein is shown to be consistent and also deductive complete with respect to Hoare's system. A subgoaler for the deductive system is described whose input is a significant subset of Pascal Programs plus inductive assertions. The output is a set of verification conditions or lemmas to be proved. Several non-trivial arithmetic and sorting programs have been shown to satisfy specifications by using an interactive theorem prover to automatically generate proofs of the verification conditions. Additional components for a more powerful verification system are under construction.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 01, 1973
Accession Number
AD0767331

Entities

People

  • David C. Luckham
  • Ralph L. London
  • Shigeru Igarashi

Organizations

  • Stanford University

Tags

Communities of Interest

  • C4I
  • Energy and Power Technologies

DTIC Thesaurus Topics

  • Arithmetic
  • Artificial Intelligence
  • Compilers
  • Computational Science
  • Computations
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Formal Languages
  • Language
  • Number Theory
  • Numbers
  • Programming Languages
  • Specifications
  • Standards
  • Theorems

Fields of Study

  • Computer science

Readers

  • Computational Linguistics
  • Mathematical Modeling and Probability Theory.

Technology Areas

  • AI & ML