Report Number: CS-TR-73-365
Institution: Stanford University, Department of Computer Science
Title: Automatic program verification I: a logical basis and its implementation.
Author: Igarashi, Shigeru
Author: London, Ralph L.
Author: Luckham, David C.
Date: May 1973
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 deduction complete with respect to Hoare's system. A subgoaler for the deduction 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.
http://i.stanford.edu/pub/cstr/reports/cs/tr/73/365/CS-TR-73-365.pdf