The verifying compiler

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

The verifying compiler: A grand challenge for computing research

Full text

Pdf (42 KB)

Source

Journal of the ACM (JACM) archive
Volume 50 , Issue 1 (January 2003) table of contents

Pages: 63 - 69

Year of Publication: 2003

ISSN:0004-5411

Author

Tony Hoare

Microsoft Research Ltd., Cambridge, UK

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 36, Downloads (12 Months): 209, Citation Count: 13

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

ABSTRACT

This contribution proposes a set of criteria that distinguish a grand challenge in science or engineering from the many other kinds of short-term or long-term research problems that engage the interest of scientists and engineers. As an example drawn from Computer Science, it revives an old challenge: the construction and application of a verifying compiler that guarantees correctness of a program before running it.

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. 1967. Assigning meanings to programs. Proc. Amer. Soc. Symp. Appl. Math. 19, 19--31.
	2	Jim Gray, What next?: A dozen information-technology research goals, Journal of the ACM (JACM), v.50 n.1, p.41-57, January 2003 [doi>10.1145/602382.602401]
	3	McCarthy, J. 1963. Towards a mathematical theory of computation. Proc. IFIP Cong. 1962. North-Holland, Amsterdam, The Netherlands.
	4	Turing, A. M. 1949. Checking a large routine. Report on a Conference on High Speed Automatic Calculating Machines. Cambridge Univ. Math. Lab. 67--69.

CITED BY 13

	Enric Rodríguez-Carbonell , Deepak Kapur, Automatic Generation of Polynomial Loop Invariants: Algebraic Foundations, Proceedings of the 2004 international symposium on Symbolic and algebraic computation, p.266-273, July 04-07, 2004, Santander, Spain
	Jonathan P. Bowen , Michael G. Hinchey, Ten commandments revisited: a ten-year perspective on the industrial application of formal methods, Proceedings of the 10th international workshop on Formal methods for industrial critical systems, p.8-16, September 05-06, 2005, Lisbon, Portugal
	Santiago Escobar, Strategies and analysis techniques in functional program optimization, AI Communications, v.17 n.1, p.35-37, January 2004
	Gary T. Leavens , Jean-Raymond Abrial , Don Batory , Michael Butler , Alessandro Coglio , Kathi Fisler , Eric Hehner , Cliff Jones , Dale Miller , Simon Peyton-Jones , Murali Sitaraman , Douglas R. Smith , Aaron Stump, Roadmap for enhanced languages and methods to aid verification, Proceedings of the 5th international conference on Generative programming and component engineering, October 22-26, 2006, Portland, Oregon, USA
	Lee Pike , Mark Shields , John Matthews, A verifying core for a cryptographic language compiler, Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications, August 15-16, 2006, Seattle, Washington
	E. Rodríguez-Carbonell , D. Kapur, Generating all polynomial invariants in simple loops, Journal of Symbolic Computation, v.42 n.4, p.443-476, April, 2007
	Domagoj Babic , Alan J. Hu, Calysto: scalable and precise extended static checking, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	Patrice Chalin, A Sound Assertion Semantics for the Dependable Systems Evolution Verifying Compiler, Proceedings of the 29th International Conference on Software Engineering, p.23-33, May 20-26, 2007
	Andrew Butterfield , Leo Freitas , Jim Woodcock, Mechanising a formal model of flash memory, Science of Computer Programming, v.74 n.4, p.219-237, February, 2009
	G. W. Hamilton, Distilling Programs for Verification, Electronic Notes in Theoretical Computer Science (ENTCS), v.190 n.4, p.17-32, November, 2007
	Alvaro E. Arenas , Juan C. Bicarregui , Tiziana Margaria, The Fmics View On The Verified Software Repository, Journal of Integrated Design & Process Science, v.10 n.4, p.47-54, December 2006
	Michael Jackson, What Can We Expect from Program Verification?, Computer, v.39 n.10, p.65-71, October 2006
	Leo Freitas , Jim Woodcock , Zheng Fu, POSIX file store in Z/Eves: An experiment in the verified software repository, Science of Computer Programming, v.74 n.4, p.238-257, February, 2009