An interpretation oriented theorem prover over integers

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

An interpretation oriented theorem prover over integers

Full text

Pdf (604 KB)

Source

Annual ACM Symposium on Theory of Computing archive
Proceedings of the second annual ACM symposium on Theory of computing table of contents

Northampton, Massachusetts, United States

Pages: 169 - 179

Year of Publication: 1970

Authors

James C. King	Thomas J. Watson Research Center, Yorktown Heights, New York
Robert W. Floyd	Stanford University, Stanford, California

Sponsor

SIGACT: ACM Special Interest Group on Algorithms and Computation Theory

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 17, Citation Count: 6

Additional Information:

abstract 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/800161.805162 What is a DOI?

ABSTRACT

A special purpose theorem prover for establishing the validity of expressions over integer variables was developed as part of a program verifier. It is built around a powerful system for manipulating and simplifying integer expressions.

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	Floyd, R. W., Assigning meanings to programs, Proc. Symp. Appl. Math., Amer. Math. Soc., Vol. 19, 1967, 19-32.
	2	Floyd, R. W., The verifying compiler, Computer Science Research Review, Carnegie-Mellon University, Annual Report, 1967, 18-19.
	3	James Cornelius King, A program verifier, 1970
	4	Davis, M., Putnam, H., and Robinson, J., The decision problem for exponential Diophantine equations, Ann. of Math. 74, 1961, 425-436.

CITED BY 6

	Zohar Manna , Richard J. Waldinger, Toward automatic program synthesis, Communications of the ACM, v.14 n.3, p.151-165, March 1971
	Robert L. Constable, On the theory of programming logics, Proceedings of the ninth annual ACM symposium on Theory of computing, p.269-285, May 04-04, 1977, Boulder, Colorado, United States
	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
	David C. Luckham, A brief account: Implementation and applications of a Pascal program verifier (Position Statement), Proceedings of the 1978 annual conference, p.786-792, January 1978
	T. E. Cheatham, Jr , Ben Wegbreit, A laboratory for the study of automating programming, ACM SIGSAM Bulletin
	T. E. Cheatham, Jr. , Ben Wegbreit, A laboratory for the study of automating programming, Proceedings of the November 16-18, 1971, fall joint computer conference, November 16-18, 1971, Las Vegas, Nevada