Verifying the correctness of compiler transformations on basic blocks using abstract interpretation

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Verifying the correctness of compiler transformations on basic blocks using abstract interpretation

Full text

Pdf (861 KB)

Source

ACM/SIGPLAN Workshop Partial Evaluation and Semantics-Based Program Manipulation archive
Proceedings of the 1991 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation table of contents

New Haven, Connecticut, United States

Pages: 106 - 115

Year of Publication: 1991

ISBN:0-89791-433-3

Also published in ...

Author

Timothy S. McNerney

Thinking Machines Corporation, 245 First Street, Cambridge, MA

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 3, Downloads (12 Months): 16, Citation Count: 2

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/115865.115877 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	Harold Abelson , Gerald Jay Sussman , Julie Sussman, Structure and interpretation of computer programs, MIT Press, Cambridge, MA, 1985
	2	Alfred V. Aho , Ravi Sethi , Jeffrey D. Ullman, Compilers: principles, techniques, and tools, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1986
	3	Zahira Ammarguellat , W. L. Harrison, III, Automatic recognition of induction variables and recurrence relations by abstract interpretation, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.283-295, June 1990, White Plains, New York, United States
	4	Andrew Berlin, A Compilation Strategy for Numerical Programs Based on Partial Evaluation, Massachusetts Institute of Technology, Cambridge, MA, 1989
	5	Boyer, R. S., and J. S. Moore, (1973), Proving Theorems About Lisp Programs, Proceedings o.f the int'l Joint Conference on Artificial Intelligence, Stanford, S.R.I., pp. 486-493.
	6	Burstali, R. M., (August 1974), Program proving as hand simulation with a little induction, Information Processing 197, North-Holland Publishing Company, Amsterdam, pp. 308-312.
	7	Chris Clack , Simon L. Peyton Jones, Strictness analysis—a practical approach, Proc. of a conference on Functional programming languages and computer architecture, p.35-49, January 1985, Nancy, France
	8	Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
	9	Curry, H. B., (1958), Combinatory Logic, v. 1, North Holland.
	10	Deutsch, L. P., (1973), An Interactive Program Verifier, Stanford University Ph.D. Thesis and Xerox PARC technical report, CSL-73-1, Palo Alto, CA.
	11	Douglas, D. C., B. Kahle, A. VasLlevsky, (1988), The Architecture o.f the CM-2 Data Processor, Technical Report HA88-1, Thinking Machines Corporation, Cambridge, MA.
	12	Gifford, D. K., P. Jouvelot, J. M. Lucassen, and M. A. Sheldon, (September 1987), FX-87 Reference Manual, MIT/LCS Technical Report 407, MIT Laboratory for Computer Science, Cambridge, MA.
	13	W D Hillis, The connection machine, MIT Press, Cambridge, MA, 1985
	14	Hinley, J. R., (1969), The principal type scheme of an object in combinatory logic, Transactions of the American Ma~h Society, v. 146, pp. 29-60.
	15	Peter B. Kessler, Discovering machine-specific code improvements, ACM SIGPLAN Notices, v.21 n.7, p.249-254, July 1986
	16	King, J. C., (1969), A program ver,ificr, Ph.D. Thesis, Carnegie-Mellon University, Pittsburg, PA.
	17	Manna, Z. (1969), The correctness of programs, Journal of Computer and System Sciences, v. 3, no. 2, pp. 119-127.
	18	Zohar Manna , Jean Vuillemin, Fixpoint approach to the theory of computation, Communications of the ACM, v.15 n.7, p.528-536, July 1972 [doi>10.1145/361454.361460]
	19	McCarthy, J. and J. A. Painter, (1967), Correctness of a Compiler for Arithmetic Expressions, Proceedings of a Symposium in Applied Mathematics, 19, Mathematical Aspects of Computer Science, American Mathematical Society, Providence, RI, pp. 33-41.
	20	Michael Metcalf , John Reid, Fortran 8x explained (revised ed.), Clarendon Press, New York, NY, 1989
	21	Milner, R., (1978), A theory of type polymorphism in prograrmning, Journal of Computer and System Sciences, v. 17, pp. 348-375.
	22	Milner, R. and R. Weyhrauch, (1972), Proving Compiler Correctness in a Mechanized Logic, Machine Intelligence 7, (Meltzer, B. and D. Mitchie, ads.), Edinburgh University Press, pp. 51-64.
	23	Alan. Mycroft , Neil. D. Jones, A relational framework for abstract interpretation, on Programs as data objects, p.156-171, April 1986, Copenhagen, Denmark
	24	J Rees , W Clinger, Revised report on the algorithmic language scheme, ACM SIGPLAN Notices, v.21 n.12, p.37-79, Dec. 1986 [doi>10.1145/15042.15043]
	25	Schonfinkel, M., (1924), Urber die Sausteine der mathematischen Logik, Mathematische A nnalen 92, pp. 305-316.
	26	Gerald J. Sussman , Guy L. Steele, Jr., An Interpreter for Extended Lambda Calculus, Massachusetts Institute of Technology, Cambridge, MA, 1975
	27	Guy L. Steele, Jr., Common LISP: the language (2nd ed.), Digital Press, Newton, MA, 1990

CITED BY 2

	Saumya Debray, Abstract interpretation and low-level code optimization, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.111-121, June 21-23, 1995, La Jolla, California, United States
	James M. Boyle , R. Daniel Resler , Victor L. Winter, Do You Trust Your Compiler?, Computer, v.32 n.5, p.65-73, May 1999