An Introduction to Proving the Correctness of Programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An Introduction to Proving the Correctness of Programs

Full text

Pdf (1.59 MB)

Source

ACM Computing Surveys (CSUR) archive
Volume 8 , Issue 3 (September 1976) table of contents

Pages: 331 - 353

Year of Publication: 1976

ISSN:0360-0300

Authors

Sidney L. Hantler	Computer Sciences Department, IBM Thomas J. Watson Research Center, Yorktown Heights, New York
James C. King	Computer Sciences Department, IBM Thomas J. Watson Research Center, Yorktown Heights, New York

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 9, Downloads (12 Months): 102, Citation Count: 37

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/356674.356677 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Robert S. Boyer , Bernard Elspas , Karl N. Levitt, SELECT—a formal system for testing and debugging programs by symbolic execution, Proceedings of the international conference on Reliable software, p.234-245, April 21-23, 1975, Los Angeles, California
	2	Robert S. Boyer , J. Strother Moore, Proving Theorems about LISP Functions, Journal of the ACM (JACM), v.22 n.1, p.129-144, Jan. 1975 [doi>10.1145/321864.321875]
	3	BURSTALL, R. M. "Some techniques for proving correctness of programs which alter data structures," Machine zntelligence 7, D. Michie (Ed.), American Elsevier, New York, 1972.
	4	CLARKE, LORI, A system to generate test data and symbolically execute programs, Report $CU-CS-060-75, Univ. of Colorado, 1975.
	5	DEUTSCH, L. P. "An interactive program verifier," PAD Dissertation, Dept. Computer Science, Univ. of Calif., Berkeley, 1973, Xerox PARC Report CSL-73-1, Palo Alto, Cahf.
	6	Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972 [doi>10.1145/356599.356602]
	7	FLOYD, R. W. "Assigning meanings to programs," in Proe. Symposium Applied Math., Vol. 19, American Mathematical Society, Providence, R.I., 1967, pp. 19-32.
	8	Elizabeth H. Wood, Consumer health on the World-Wide Web: gold or gilt?, Health Care on the Internet, v.1 n.1, p.59-72, 1997 [doi>10.1300/J138v01n01_06]
	9	GOOD, D. I.; AND RAGLAND, L. C. "Nueleus--a language of provable programs," in Program test methods, W. Hetzel (Ed.), Prentice-Hall inc., Englewood Cliffs, N.J., 1973, pp. 93-117.
	10	HOARE, C. A. R.; AND WIRTH, N. "An axiomatic definition of the programming language PASCAL," Acta informatzca 2, (1973), 335-355.
	11	Shigeru Igarashi , Ralph L. London , David C. Luckham, Automatic program verification I: a logical basis and its implementation., Stanford University, Stanford, CA, 1973
	12	KATZ, S. M.; AND MANNA, Z. "A heuristic approach to program verification," in Proc. Third Internatl. Joint Conf. on Artzficial Intelligence, SRI Publications Dept. Stanford Calif., 1973, pp. 500-512.
	13	KINO, j.C. "Proving programs to be correct," IEEE Trans on Computers C-20, 11, (Nov. 1971), 1331-1336.
	14	James Cornelius King, A program verifier, 1970
	15	James C. King, A new approach to program testing, Proceedings of the international conference on Reliable software, p.228-233, April 21-23, 1975, Los Angeles, California
	16	James C. King, Symbolic execution and program testing, Communications of the ACM, v.19 n.7, p.385-394, July 1976 [doi>10.1145/360248.360252]
	17	Ralph L. London, The current state of proving programs correct, Proceedings of the ACM annual conference, p.39-46, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800193.805820]
	18	Zohar Manna, Mathematical Theory of Computation, Dover Publications, Incorporated, 2003
	19	Derek C. Oppen , Stephen A. Cook, Proving assertions about programs that manipulate data structures, Proceedings of seventh annual ACM symposium on Theory of computing, p.107-116, May 05-07, 1975, Albuquerque, New Mexico, United States [doi>10.1145/800116.803758]
	20	Norihisa Suzuki, Verifying programs by algebraic and logical reduction, Proceedings of the international conference on Reliable software, p.473-481, April 21-23, 1975, Los Angeles, California
	21	TOPOR, R.W. "Interactive program verification using virtual programs," PhD Dissertation, Univ. of Edinburgh, Edinburgh, Scotland, 1975.
	22	Ben Wegbreit, The synthesis of loop predicates, Communications of the ACM, v.17 n.2, p.102-113, Feb. 1974 [doi>10.1145/360827.360850]
	23	Ben Wegbreit , Jay M. Spitzen, Proving Properties of Complex Data Structures, Journal of the ACM (JACM), v.23 n.2, p.389-396, April 1976 [doi>10.1145/321941.321957]

CITED BY 37

	Laura K. Dillon, Using symbolic execution for verification of Ada tasking programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.12 n.4, p.643-669, Oct. 1990
	Erhard Ploedereder, Pragmatic techniques for program analysis and verification, Proceedings of the 4th international conference on Software engineering, p.63-72, September 17-19, 1979, Munich, Germany
	James C. King, Tutorial session 3B: Prospects for program verification, Proceedings of the 3rd international conference on Software engineering, p.71, May 10-12, 1978, Atlanta, Georgia, United States
	Ted J. Biggerstaff, Factored Specifications In The Synthesis Of LISP Functions, Proceedings of the 1978 annual conference, p.393-402, December 04-06, 1978, Washington, D.C., United States
	Clarence A. Ellis , Gary J. Nutt, Office Information Systems and Computer Science, ACM Computing Surveys (CSUR), v.12 n.1, p.27-60, March 1980
	J. Mack Adams , James Armstrong , Melissa Smartt, Assertional checking and symbolic execution: An effective combination for debugging, Proceedings of the 1979 annual conference, p.152-156, January 1979
	Kien A. Hua , Jacob A. Abraham, Design of sytems with concurrent error detection using software redundancy, Proceedings of 1986 ACM Fall joint computer conference, p.826-835, November 1986, Dallas, Texas, United States
	Laura K. Dillon, Verifying General Safety Properties of Ada Tasking Programs, IEEE Transactions on Software Engineering, v.16 n.1, p.51-63, January 1990
	Tevfik Bultan , Richard Gerber , William Pugh, Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results, ACM Transactions on Programming Languages and Systems (TOPLAS), v.21 n.4, p.747-789, July 1999
	Timothy E. Lindquist , Jeffrey L. Facemire, Ada-based abstract machine specification of CAIS to generate validation tests, Proceedings of the second annual Washington Ada symposium on Ada: Ada in the mainstream: applications and education, p.173-178, March 1985, Washington, D. C., United States
	M. Agrawala , D. L. Jain, Comments on 'Temporal Logic-Based Deadlock Analysis for Ada' by G.M. Karam and R.J.A. Burh, IEEE Transactions on Software Engineering, v.19 n.2, p.198-199, February 1993
	W. Richards Adrion , Martha A. Branstad , John C. Cherniavsky, Validation, Verification, and Testing of Computer Software, ACM Computing Surveys (CSUR), v.14 n.2, p.159-192, June 1982
	Iris Vessey , Ron Weber, Some factors affecting program repair maintenance: an empirical study, Communications of the ACM, v.26 n.2, p.128-134, Feb. 1983
	John A. Sharp, Data oriented program design, ACM SIGPLAN Notices, v.15 n.9, p.44-57, September 1980
	Patrick Cousot , Radhia Cousot, Automatic synthesis of optimal invariant assertions: Mathematical foundations, ACM SIGPLAN Notices, v.12 n.8, p.1-12, August 1977
	K. Culik , M. M. Rizki, Logic versus mathematics in computer science education, ACM SIGCSE Bulletin, v.15 n.1, p.14-20, February 1983
	C. V. Ramamoorthy , F. B. Bastani , J. M. Favaro , Y. R. Mok , C. W. Nam , K. Suzuki, A systematic approach to the development and validation of critical software for nuclear power plants, Proceedings of the 4th international conference on Software engineering, p.231-240, September 17-19, 1979, Munich, Germany
	T. Y. Chen , T. H. Tse , Zhiquan Zhou, Semi-proving: an integrated method based on global symbolic evaluation and metamorphic testing, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	Ronald L. Davis, “Recommended mathematical topics for computer science majors”, ACM SIGCSE Bulletin, v.9 n.3, p.51-55, Aug 1977
	Ali Mili , Jules Desharnais, A system for classifying program verification methods: Assigning meanings to program verification methods, Proceedings of the 7th international conference on Software engineering, p.499-509, March 26-29, 1984, Orlando, Florida, United States
	S. J. Zeil , E. C. Epp, Interpretation in a tool-fragment environment, Proceedings of the 10th international conference on Software engineering, p.241-248, April 11-15, 1988, Singapore
	W. E. Cory, Symbolic simulation for functional verification with ADLIB and SDL, Proceedings of the 18th conference on Design automation, p.82-89, June 29-July 01, 1981, Nashville, Tennessee, United States
	Tom Towle , Tom DeFanti, GAIN: An interactive program for teaching interactive computer graphics programming, ACM SIGGRAPH Computer Graphics, v.12 n.3, p.54-59, August 1978
	Michael Young , Richard N. Taylor, Rethinking the taxonomy of fault detection techniques, Proceedings of the 11th international conference on Software engineering, p.53-62, May 1989, Pittsburgh, Pennsylvania, United States
	B. Randell , P. Lee , P. C. Treleaven, Reliability Issues in Computing System Design, ACM Computing Surveys (CSUR), v.10 n.2, p.123-165, June 1978
	Gerald M. Karam , Raymond J. A. Buhr, Temporal Logic-Based Deadlock Analysis for Ada, IEEE Transactions on Software Engineering, v.17 n.10, p.1109-1125, October 1991
	Timothy E. Lindquist , Joyce R. Jenkins, Test-Case Generation with IOGen, IEEE Software, v.5 n.1, p.72-79, January 1988
	Arthur Sedgwick, Structuring control in Fortran, ACM SIGPLAN Notices, v.12 n.11, p.55-60, November 1977
	Kostas Kontogiannis, Toward program representation and program understanding using process algebras, Proceedings of the 1992 conference of the Centre for Advanced Studies on Collaborative research, November 09-12, 1992, Toronto, Ontario, Canada
	M. Young , R. M. Taylor, Combining Static Concurrency Analysis with Symbolic Execution, IEEE Transactions on Software Engineering, v.14 n.10, p.1499-1511, October 1988
	James C. King, Program reduction using symbolic execution, ACM SIGSOFT Software Engineering Notes, v.6 n.1, p.9-14, January 1981
	Stephen F. Siegel , Anastasia Mironova , George S. Avrunin , Lori A. Clarke, Using model checking with symbolic execution to verify parallel numerical programs, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
	Lori A. Clarke , David S. Rosenblum, A historical perspective on runtime assertion checking in software development, ACM SIGSOFT Software Engineering Notes, v.31 n.3, May 2006
	K. Culik, On formal and informal proofs for program correctness, ACM SIGPLAN Notices, v.18 n.1, p.23-28, January 1983
	C. Koutsikas , N. Malevris, A new script language applicable to symbolic execution systems, International Journal of Computers and Applications, v.28 n.1, p.1-11, January 2006
	C. Koutsikas , N. Malevris, A new script language applicable to symbolic execution systems, International Journal of Computers and Applications, v.28 n.1, p.1-11, January 2006
	Stephen F. Siegel , Anastasia Mironova , George S. Avrunin , Lori A. Clarke, Combining symbolic execution with model checking to verify parallel numerical programs, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-34, April 2008