Advertisement

The Verifying Compiler: A Grand Challenge for Computing Research

  • Tony Hoare
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2890)

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.

Keywords

Model Check Grand Challenge Computing Research Legacy Code Legacy Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Gray, J.: What Next? A Dozen Information-technology Research Goals, MS-TR-50, Microsoft Research (June 1999)Google Scholar
  2. 2.
    Leino, K.M., Nelson, G.: An extended static checker for Modula-3. Compiler. In: Koskimies, K. (ed.) CC 1998. LNCS, vol. 1383, pp. 302–305. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  3. 3.
    Meyer, B.: Object-Oriented Software Construction, 2nd edn. Prentice-Hall, Englewood Cliffs (1997)zbMATHGoogle Scholar
  4. 4.
    Hall, A., Chapman, R.: Correctness by Construction: Developing a Commercial Secure System. IEEE Software 19(1), 18–25 (2002)CrossRefGoogle Scholar
  5. 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. 6.
    A congressional statement presented by the director of the National Infrastructure Protection Center See, http://www.fbi.gov/congress/congress02/nipc072402.htm
  7. 7.
    Schneider, F.B. (ed.): Trust in Cyberspace, Committee on Information Systems Trustworthiness, National Research Council (1999)Google Scholar
  8. 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. 9.
    Gates, W.H.: Internal communication, Microsoft Corporation (2002)Google Scholar
  10. 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. 11.
    Necula, G.: Proof-carrying code. In: Proceedings of the 24th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1997) (January 1997)Google Scholar
  12. 12.
    Turing, A.M.: Checking a large routine. In: Report on a Conference on High Speed Automatic Calculating machines, pp. 67–69. Cambridge University Math. Lab. (1949)Google Scholar
  13. 13.
    McCarthy, J.: Towards a mathematical theory of computation. In: Proc. IFIP Cong. 1962. North Holland, Amsterdam (1963)Google Scholar
  14. 14.
    Floyd, R.W.: Assigning meanings to programs. Proc. Amer. Soc. Symp. Appl. Math. 19, 19–31 (1967)MathSciNetGoogle Scholar
  15. 15.
    King, J.C.: A Program Verifier, PhD thesis, Carnegie-Mellon University (1969)Google Scholar
  16. 16.
    Stroustrup, B.: The C++ Programming Language. Adison-Wesley, Reading (1985)Google Scholar
  17. 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. 18.
    Haskell 98 language and libraries: the Revised Report. Journal of Functional Programming 13(1) (January 2003)Google Scholar
  19. 19.
    Hoare, C.A.R.: Assertions, Marktoberdorf Summer School (2002) (to appear)Google Scholar
  20. 20.
    Stepney, S., Cooper, D., Woodcock, J.C.P.W.: An Electronic Purse: Specification, Refinement, and Proof, PRG-126. Oxford University Computing Laboratory, Oxford (July 2000)Google Scholar
  21. 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. 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. 23.
    Evans, D., Larochelle, D.: Improving Security Using Extensible Lightweight Static Analysis. IEEE Software (January/February 2002)Google Scholar
  24. 24.
    Hallem, S., Chelf, B., Xie, Y., Engler, D.: A System and Language for Building System-Specific Static Analyses. PLDI (2002)Google Scholar
  25. 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. 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. 27.
    Evans, D.: Static detection of dynamic memory errors. In: SIGPLAN Conference on Programming Languages Design and Implementation (1996)Google Scholar
  28. 28.
    Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  29. 29.
    Ruf, E.: Context-sensitive alias analysis reconsidered. Sigplan Notices 30(6) (June 1995)Google Scholar
  30. 30.
    Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)Google Scholar
  31. 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. 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. 33.
    Shankar, N.: Machine-assisted verification using theorem-proving and model checking. In: Mathematical Methods of Program Development, NATO ASI, vol. 138, pp. 499–528. Springer, Heidelberg (1997)Google Scholar
  34. 34.
    Gordon, M.J.C.: HOL: A proof generating system for Higher-Order Logic. In: VLSI Specification, Verification and Synthesis, pp. 73–128. Kluwer, Dordrecht (1988)Google Scholar
  35. 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)CrossRefGoogle Scholar
  36. 36.
    Moskewicz, M., Madigan, C., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: 38th Design Automation Conference (DAC2001), Las Vegas (June 2001)Google Scholar
  37. 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)CrossRefGoogle Scholar
  38. 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. 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)CrossRefGoogle Scholar
  40. 40.
    Milner, R.: Communicating and Mobile Systems: the pi Calculus, CUP (1999)Google Scholar
  41. 41.
    Roscoe, A.W.: Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)Google Scholar
  42. 42.
    Chandy, K.M., Misra, J.: Parallel Program Design: a Foundation. Addison-Wesley, Reading (1988)zbMATHGoogle Scholar
  43. 43.
    O’Hearn, P., Reynolds, J., 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)CrossRefGoogle Scholar
  44. 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)CrossRefGoogle Scholar
  45. 45.
    Stepanov, A., Lee, M.: Standard Template Library. Hewlett Packard (1994)Google Scholar
  46. 46.
    Hoare, C.A.R.: The Verifying Compiler: a Grand Challenge for Computer Research. JACM 1(50), 63–69 (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Tony Hoare
    • 1
  1. 1.Microsoft Research Ltd.CambridgeUK

Personalised recommendations