Title :
An Exercise in Automatic Program Verification
Author_Institution :
Artificial Intelligence Laboratory, Stanford University
Abstract :
This paper describes in some detail the computer-aided proof of a permutation program obtained using the Stanford Pascal verifier. We emphasize the systematic way in which a proof can be developed from an intuitive understanding of the program. The paper fillustrates the current state of the art in automatic program verification.
Keywords :
Assertion language; automatic program verification; inductive assertions; pennutation; theorem proving; Artificial intelligence; Lead; Assertion language; automatic program verification; inductive assertions; pennutation; theorem proving;
Journal_Title :
Software Engineering, IEEE Transactions on
DOI :
10.1109/TSE.1979.230183
