On specifying verifiers

ABSTRACT

The goal of automatic program verification is to prove programs correct formally. We argue that the existing notions of formal proof are too syntactic and as such too intimately bound up with details of low-level computation. We propose a more semantic notion of formal proof which nevertheless pays due respect to the problem of effectiveness in proof checking. Such a notion supplies a more practical basis for the specification of verifiers than do extant approaches. In particular the problem of constructing verifiers according to our approach is reduced entirely to routine development and implementation of decision methods, while permitting shorter proofs and yet remaining easy to develop proofs with.

REFERENCES

• 1: Constable, R. L. and M. O'Donnell, A Programming Logic, Winthrop Press, 1978.
• 2: Cook, S. A., and R. A. Reckhow, The Relative Efficiency of Propositional Proof Systems, J. Symbolic Logic, 44, 1, 36-50, March, 1979.
• 3: Richard A. De Millo , Richard J. Lipton , Alan J. Perlis, Social processes and proofs of theorems and programs, Communications of the ACM, v.22 n.5, p.271-280, May 1979 [doi>10.1145/359104.359106]
• 4: Floyd, R. W., Assigning Meanings to Programs, In Mathematical Aspects of Computer Science (ed. J. T. Schwartz), 19-32, 1967.
• 5: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 6: James Cornelius King, A program verifier, 1970
• 7: Lewis, H., Complexity of Solvable Cases of the Decision Problem for the Predicate Calculus, 19th Annual Symposium on Foundations of Computer Science, Ann Arbor, Michigan, Oct., 1978.
• 8: Greg Nelson , Derek C. Oppen, A simplifier based on efficient decision algorithms, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.141-150, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512775]
• 9: Newman, J. R., The World of Mathematics, Simon and Schuster, NY, 1956.
• 10: Robert L. Ashenhurst, ACM forum, Communications of the ACM, v.22 n.11, p.621-630, Nov. 1979 [doi>10.1145/359168.359177]
• 11: Pratt, V. R., Axioms or Algorithms, Proceedings of the Eighth Symposium on Mathematical Foundations of Computer Science, Olomouc, Czechoslovakia, Sept., 1979.