Issue No.05 - September (1979 vol.5)
W. Polak , Artificial Intelligence Laboratory, Stanford University
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.
theorem proving, Assertion language, automatic program verification, inductive assertions, pennutation
W. Polak, "An Exercise in Automatic Program Verification", IEEE Transactions on Software Engineering, vol.5, no. 5, pp. 453-458, September 1979, doi:10.1109/TSE.1979.230183