Skip to main content
SpringerLink
Log in
Book cover

Joint Modular Languages Conference

JMLC 2003: Modular Programming Languages pp 25–35Cite as

The Verifying Compiler: A Grand Challenge for Computing Research

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2789))

Abstract

I propose a set of criteria which 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, I revive an old challenge: the construction and application of a verifying compiler that guarantees correctness of a program before running it.

Reprinted with the kind allowance of Springer Verlag from the proceedings of ECOOP 2003, LNCS 2743

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Gray, J.: What Next? A Dozen Information-technology Research Goals, MS-TR-50, Microsoft Research (June 1999)

    Google Scholar 

  2. Leino, K.M., Nelson, G.: An extended static checker for Modula-3. In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 302–305. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  3. Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)

    MATH  Google Scholar 

  4. Hall, A., Chapman, R.: Correctness by Construction: Developing a Commercial Secure System. IEEE Software 19(1), 18–25 (2002)

    Article  Google Scholar 

  5. Jim, T., Morrisett, G., Grossman, D., Hicks, M., Cheney, J., Wang, Y.: Cyclone: A safe dialect of C. In: USENIX Annual Technical Conference, Monterey, CA (June 2002)

    Google Scholar 

  6. See http://www.fbi.gov/congress/congress02/nipc072402.htm a congressional statement presented by the director of the National Infrastructure Protection Center

  7. Schneider, F.B. (ed.): Trust in Cyberspace, Committee on Information Systems Trustworthiness, National Research Council (1999)

    Google Scholar 

  8. Wagner, D., Foster, J., Brewer, E., Aiken, A.: A first step towards automated detection of buffer overrun vulnerabilities. In: Network and Distributed System Security Symposium, San Diego, CA (February 2000)

    Google Scholar 

  9. Gates, W.H.: internal communication. Microsoft Corporation (2002)

    Google Scholar 

  10. Planning Report 02-3. The Economic Impacts of Inadequate Infrastructure for Software Testing, prepared by RTI for NIST, US Department of Commerce (May 2002)

    Google Scholar 

  11. Necula, G.: Proof-carrying code. In: Proceedings of the 24th Annual ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL 1997) (January 1997)

    Google Scholar 

  12. Turing, A.M.: Checking a large routine. In: Report on a Conference on High Speed Automatic Calculating machines, Cambridge University Math. Lab., pp. 67–69 (1949)

    Google Scholar 

  13. McCarthy, J.: Towards a mathematical theory of computation. In: Proc. IFIP Cong. 1962. North-Holland, Amsterdam (1963)

    Google Scholar 

  14. Floyd, R.W.: Assigning meanings to programs. Proc. Amer. Soc. Symp. Appl. Math. 19, 19–31 (1967)

    MathSciNet  Google Scholar 

  15. King, J.C.: A Program Verifier, PhD thesis, Carnegie-Mellon University (1969)

    Google Scholar 

  16. Stroustrup, B.: The C++ Programming Language. Addison-Wesley, Reading (1985)

    Google Scholar 

  17. Igarashi, A., Pierce, B., Wadler, P.: Featherweight Java: A Minimal Core Calculus for Java and GJ. In: OOPSLA 1999, pp. 132–146 (1999)

    Google Scholar 

  18. Haskell 98 language and libraries: the Revised Report, Journal of Functional Programming 13(1) (January 2003)

    Google Scholar 

  19. Hoare, C.A.R.: Assertions, Marktoberdorf Summer School (2002) (to appear)

    Google Scholar 

  20. Stepney, S., Cooper, D., Woodcock, J.C.P.W.: An Electronic Purse: Specification, Refinement, and Proof, PRG-126. Oxford University Computing Laboratory, Oxford (2000)

    Google Scholar 

  21. Galloway, A.J., Cockram, T.J., McDermid, J.A.: Experiences with the application of discrete formal methods to the development of engine control software, Hise York (1998)

    Google Scholar 

  22. Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software – Practice and Experience (30), 775–802 (2000)

    Google Scholar 

  23. Evans, D., Larochelle, D.: Improving Security Using Extensible Lightweight Static Analysis. IEEE Software (January/February 2002)

    Google Scholar 

  24. Hallem, S., Chelf, B., Xie, Y., Engler, D.: A System and Language for Building System- Specific Static Analyses. In: PLDI 2000 (2002)

    Google Scholar 

  25. Necula, G.C., McPeak, S., Weimer, W.: CCured: Type-safe retrotting of legacy code. In: 29th ACM Symposium on Principles of Programming Languages, Portland, OR (January 2002)

    Google Scholar 

  26. Shankar, U., Talwar, K., Foster, J.S., Wagner, D.: Detecting format string vulnerabilities with type qualifiers. In: Proceedings of the 10th USENIX Security Symposium (2001)

    Google Scholar 

  27. Evans, D.: Static detection of dynamic memory errors. In: SIGPLAN Conference on Programming Languages Design and Implementation (1996)

    Google Scholar 

  28. Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  29. Ruf, E.: Context-sensitive alias analysis reconsidered. Sigplan Notices 30(6) (June 1995)

    Google Scholar 

  30. Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)

    Google Scholar 

  31. Roscoe, A.W.: Model-Checking CSP, A Classical Mind: Essays in Honour of C.A.R. Hoare, pp. 353–378. Prentice-Hall International, Englewood Cliffs (1994)

    Google Scholar 

  32. Musuvathi, M., Park, D.Y.W., Chou, A., Engler, D.R., Dill, D.L.: CMC: A pragmatic approach to model checking real code. In: OSDI 2002 (2002) (to appear)

    Google Scholar 

  33. Shankar, N.: Machine-assisted verification using theorem-proving and model checking, Mathematical Methods of Program Development. In: NATO ASI, vol. 138, pp. 499–528. Springer, Heidelberg (1997)

    Google Scholar 

  34. Gordon, M.J.C.: HOL: A proof generating system for Higher-Order Logic, VLSI Specification, Verification and Synthesis, pp. 73–128. Kluwer, Dordrecht (1988)

    Google Scholar 

  35. Shankar, N.: PVS: Combining specification, proof checking, and model checking. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 257–264. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  36. Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: 38th Design Automation Conference (DAC 2001), Las Vegas (June 2001)

    Google Scholar 

  37. Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  38. Nimmer, J.W., Ernst, M.D.: Automatic generation of program specifications. In: Proceedings of the 2002 International Symposium on Software Testing and Analysis, pp. 232–242 (2002)

    Google Scholar 

  39. Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for eSC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  40. Milner, R.: Communicating and Mobile Systems: the pi Calculus, CUP (1999)

    Google Scholar 

  41. Roscoe, A.W.: Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)

    Google Scholar 

  42. Chandy, K.M., Misra, J.: Parallel Program Design: a Foundation. Addison-Wesley, Reading (1988)

    MATH  Google Scholar 

  43. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  44. Hoare, C.A.R., Jifeng, H.: A trace model for pointers and objects. In: Guerraoui, R. (ed.) ECOOP 1999. LNCS, vol. 1628, pp. 1–17. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  45. Stepanov, A.: Meng Lee, Standard Template Library, Hewlett Packard (1994)

    Google Scholar 

  46. Hoare, C.A.R.: The Verifying Compiler: a Grand Challenge for Computer Research. JACM 50(1), 63–69 (2003)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Research Ltd., 7 J.J. Thomson Ave, Cambridge, CB3 0FB, UK

    Tony Hoare

Authors
  1. Tony Hoare
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. No Affiliation,  

    László Böszörményi

  2. fürWirtschaftswissenschaften und Informatik, Universität Klagenfurt, Fakultät, Universitätsstraße 65-67, 9020, Klagenfurt, Austria

    Peter Schojer

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hoare, T. (2003). The Verifying Compiler: A Grand Challenge for Computing Research. In: Böszörményi, L., Schojer, P. (eds) Modular Programming Languages. JMLC 2003. Lecture Notes in Computer Science, vol 2789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45213-3_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45213-3_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40796-6

  • Online ISBN: 978-3-540-45213-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation