Accession Number:
AD0767331
Title:
Automatic Program Verification 1: A Logical Basis and Its Implementation
Descriptive Note:
Corporate Author:
STANFORD UNIV CA DEPT OF COMPUTER SCIENCE
Personal Author(s):
Report Date:
1973-05-01
Pagination or Media Count:
58.0
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 Hoares 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.
Descriptors:
Subject Categories:
- Computer Programming and Software