The Community for Technology Leaders
Green Image
Issue No. 05 - September (1979 vol. 5)
ISSN: 0098-5589
pp: 453-458
W. Polak , 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.
INDEX TERMS
theorem proving, Assertion language, automatic program verification, inductive assertions, pennutation
CITATION
W. Polak, "An Exercise in Automatic Program Verification", IEEE Transactions on Software Engineering, vol. 5, no. , pp. 453-458, September 1979, doi:10.1109/TSE.1979.230183
99 ms
(Ver )