Abstract
The generation of verification conditions is one of the basic steps in proving the correctness of programs. Alternative methods for generating verification conditions have been developed and used, each technique apparently quite different from the others. This paper presents three of the most well-known methods and shows how they relate to each other and to the basic program analysis task.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Basu, S. K. and Yeh, R. T. Strong verification of Programs. Soft. Eng. and Sys. Lab., Univ. of Texas-Austin, Techn. Report SESLTR-13, 1975.
Boyer, R. S. and Moore, J. S. Proving theorems about Lisp functions. JACM, vol. 22, no. 1, January 1975, pp. 48 - 59.
Burstall, R. M. Program proving as hand simulation with a little induction. Information Processing 74, Proceedings of IFIP Congress 74, J. L. Rosenfeld, ed., North-Holland, 308-312, 1974.
Chamberlan, Donald D. The single assignment approach to parallel processing. FJCC, Las Vegas, Nov. 1971. pp 263 - 269.
Darlington, John. A semantic approach to automatic program improvement, Ph.D. dissertation, Univ. of Edinburgh, 1973.
Deutsch, L. P. An Interactive Program Verifier. Ph.D. dissertation, Dept. Comp. Sci., Univ. of Calif., Berkeley CA., May 1973. (Also Xerox PARC Report CSL-73-1, Palo Alto, CA. )
Dijkstra, E. W. Guarded commands, non-determinacy and a calculus for the derivation of programs. CACM, vol. 18, no. 8, August 1975, pp. 453 - 457.
Elspas, B. et al. An assessment of techniques for proving program correctness, Comp. Surveys, Vol. 4, No. 2, June 1972, pp. 97 - 147.
Floyd, R. W. Assigning meanings to programs, Proc. Symp. Appl. Math., Amer. Math. Soc., vol. 19, pp. 19 - 32, 1967.
Good, D. I. Towards a man-machine system for proving program correctness. Ph.D dissertation, Univ. of Wisc., 1970.
Hoare, C. A. R. An axiomatic basis for computer programming. CACM, vol. 12. no. 10, Oct. 1969, pp. 576 - 583.
King, J. C. Proving programs to be correct, IEEE Trans. on Comp., Vol. C-20, No. 11, November 1971, pp. 1331 - 1336.
King, J. C. A Program Verifier. Ph.D. dissertation, Carnegie-Mellon Univ., Pittsburgh, Pa., 1969.
King, J. C. A new approach to program testing, 1975 Int. Conf. on Reliable Software, April 1975, pp. 228-233. (Also appears in Programming Methodology, Lect. Notes in Comp. Sci., 23, Springer-Verlag, 1974, 278-290.)
Manna, Z. Introduction to Mathematical Theory of Computation, McGraw-Hill Book Company, New York, N. Y., 1974.
Naur, P. Proof of algorithms by general snapshots. BIT 6, 4, 1966, pp. 310 - 316.
Topor, R. W. Interactive Program Verification Using Virtual Programs. Ph.D. dissertation, Dept. of AI, Univ. of Edinburgh, 1975.
Waldinger, R. J. and Levitt, K. N. Reasoning about programs. Artif. Intell., 5, 3, 1974, pp. 235 - 316.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1976 Springer-Verlag Berlin · Heidelberg
About this paper
Cite this paper
King, J.C. (1976). On Generating Verification Conditions for Correctness Proofs. In: Schneider, HJ., Nagl, M. (eds) Programmiersprachen. Informatik-Fachberichte, vol 1. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-66319-2_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-66319-2_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-07619-3
Online ISBN: 978-3-642-66319-2
eBook Packages: Springer Book Archive