Philosophy of Computer Science

Can Programs Be Verified?

Last Update: 12 April 2007

Note: NEW or UPDATED material is highlighted

This is an archival version. The latest version is located at:
http://www.cse.buffalo.edu/~rapaport/584/canprogsbeverified.html

"I hold the opinion that the construction of computer programs is a mathematical activity like the solution of differential equations, that programs can be derived from their specifications through mathematical insight, calculation, and proof, using algebraic laws as simple and elegant as those of elementary arithmetic."

"Computer programming is an exact science in that all the properties of a program and all the consequences of executing it in any given environment can, in principle, be found out from the text of the program itself by means of purely deductive reasoning."

"When the correctness of a program, its compiler, and the hardware of the computer have all been established with mathematical certainty, it will be possible to place great reliance on the results of the program, and predict their properties with a confidence limited only by the reliability of the electronics."—C.A.R. Hoare

  1. McCarthy, John (1963), "Towards a Mathematical Science of Computation", in C.M. Popplewell (ed.), Information Processing 1962: Proceedings of DFIP Congress 62 (Amsterdam: North-Holland): 21-28; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 35-56.

  2. Naur, Peter (1966), "Proof of Algorithms by General Snapshots", BIT 6: 310-316; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 57-64.

  3. Floyd, Robert W. (1967), "Assigning Meanings to Programs", in Mathematical Aspects of Computer Science: Proceedings of Symposia in Applied Mathematics, Vol. 19 (American Mathematical Society): 19-32; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 65-81.

  4. Hoare, C.A.R. (1969), "An Axiomatic Basis for Computer Programming", Communications of the ACM 12: 576-580, 583; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 83-96.

  5. Dijkstra, Edsgar W. (1974), "Programming as a Discipline of Mathematical Nature", American Mathematical Monthly (June-July): 608-612.

  6. Dijkstra, Edsgar W. (1975), "Guarded Commands, Nondeterminacy and Formal Derivation of Programs", Communications of the ACM 18(8): 453-457

  7. De Millo, Richard A.; Lipton, Richard J.; & Perlis, Alan J. (1979), "Social Processes and Proofs of Theorems and Programs", Communications of the ACM 22(5): 271-280; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 297-319.

  8. Naur, Peter (1982), "Formalization in Program Development", BIT 22: 437-453; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 191-210.

  9. Dijkstra, Edsger W. (1983), "Fruits of Misunderstanding" (EWD-854), reprinted in Datamation (15 February 1985): 86-87.

  10. Scherlis, William L.; & Scott, Dana S. (1983), "First Steps towards Inferential Programming", in R.E.A. Mason (ed.), Information Processing 83 (JFIP and Elsevier Science Publishers): 199-212; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 99-133.

  11. Olson, Steve (1984, January/February), "Sage of Software", Science: 75-80.

  12. Gries, David (1981), The Science of Programming (New York: Springer-Verlag).

  13. Meyer, Bertrand (1985), "On Formalism in Specifications", IEEE Software 2(1) (January): 6-26; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 155-189.

  14. Smith, Brian Cantwell (1985), "Limits of Correctness in Computers" [PDF], Technical Report CSLI-85-36 (Stanford, CA: Center for the Study of Language and Information); first published in Charles Dunlop & Rob Kling (eds.), Computerization and Controversy (San Diego: Academic Press, 1991): 632-646; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 275-293.

    1. Also see:
      Fetzer, James H. (1999),       "The Role of Models in Computer Science" [PDF], The Monist 82(1): 20-36.

    2. Also possibly of relevance:
      Jackson, Michael (2003),       "Why Software Writing Is Difficult and Will Remain So" [PDF], Information Processing Letters 88: 13-25.

    3. NEW
      For more examples like Smith's moon-mistaken-as-missile, only with more dire consequences, see:
      Neumann, Peter G. (1993), "Modeling and Simulation", Communications of the ACM 36(4) (June): 124.

    4. NEW
      Another interesting article on computational modeling (and what can go wrong):
      Hayes, Brian (2007), "Calculating the Weather", American Scientist 95(3) (May-June): 271-273.

    5. NEW
      On the nature of abstraction, see:

      1. Rapaport, William J. (1999), "Implementation Is Semantic Interpretation" [PDF], The Monist 82(1): 109-130.

      2. Kramer, Jeff (2007), "Is Abstraction the Key to Computing?", Communications of the ACM 50(4) (April): 36-42.

  15. Verity, John W. (1985), "Bridging the Software Gap", Datamation (15 February): 84, 88.

  16. Hoare, C.A.R. (1986), "Mathematics of Programming", Byte (August); reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 135-154.

  17. Floyd, Christiane (1987), "Outline of a Paradigm Change in Software Engineering", in G. Bjerknes et al. (eds.), Computers and Democracy: A Scandinavian Challenge (Brookfield, VT: Gower Publishing): 191-210; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 239-259.

  18. Fetzer, James H. (1988), "Program Verification: The Very Idea", Communications of the ACM 31(9) (September): 1048-1063; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 321-358.

    1. Ardis, Mark; Basili, Victor; Gerhart, Susan; Good, Donald; Gries, David; Kemmerer, Richard; Leveson, Nancy; Musser, David; Neumann, Peter; & von Henke, Friedrich (1989), "Editorial Process Verification" (letter to the editor, with replies by James H. Fetzer and Peter J. Denning), ACM Forum, Communications of the ACM 32(3) (March): 287-290.

    2. Pleasant, James C.; AND Paulson, Lawrence; Cohen, Avra; & Gordon, Michael; AND Bevier, William R.; Smith, Michael K.; & Young, William D.; AND Clune, Thomas R.; AND Savitzky, Stephen (1989), "The Very Idea" (5 letters to the editor), Technical Correspondence, Communications of the ACM 32(3) (March): 374-377.

    3. Fetzer, James H. (1989), "Program Verification Reprise: The Author's Response" (to the above 5 letters), Technical Correspondence, Communications of the ACM 32(3) (March): 377-381.

    4. Dobson, John; & Randell, Brian (1989), "Program Verification: Public Image and Private Reality", Communications of the ACM 32(4) (April): 420-422.

    5. Müller, Harald M.; AND Holt, Christopher M.; AND Watters, Aaron (1989), "More on the Very Idea" (3 letters to the editor, with reply by James H. Fetzer), Technical Correspondence, Communications of the ACM 32(4) (April): 506-512.

    6. Hill, Richard; AND Conte, Paul T.; AND Parsons, Thomas W.; AND Nelson, David A. (1989), "More on Verification" (4 letters to the editor), ACM Forum, Communications of the ACM 32(7) (July): 790-792.

    7. Tompkins, Howard E. (1989), "Verifying Feature-Bugs" (letter to the editor), Technical Correspondence, Communications of the ACM 32: 1130-1131.

      • Note: This does not seem to be available on-line.

  19. Barwise, Jon (1989), "Mathematical Proofs of Computer System Correctness" [PDF], Notices of the American Mathematical Society 36: 844-851.

      Included in the online version of the above:
    • Dudley, Richard (1990), "Program Verification" (letter to Jon Barwise (ed.), Computers and Mathematics column, with a reply by Barwise), Notices of the American Mathematical Society 37: 123-124.

  20. Blum, Bruce I. (1989), "Formalism and Prototyping in the Software Process", Information and Decision Technologies 15: 327-341; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 213-238.

  21. Cohen, Avra (1989), "The Notion of Proof in Hardware Verification", Journal of Automated Reasoning 5: 127-139; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 359-374.

  22. Colburn, Timothy R. (1991), "Program Verification, Defeasible Reasoning, and Two Views of Computer Science", Minds and Machines 1: 97-116; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 375-399.

  23. Fetzer, James H. (1991), "Philosophical Aspects of Program Verification", Minds and Machines 1: 197-216; reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 403-427.

  24. Devlin, Keith (1992), "Computers and Mathematics", Notices of the American Mathematical Society 39: 1065-1066.

  25. MacKenzie, Donald (1992), "Computers, Formal Proofs, and the Law Courts", Notices of the American Mathematical Society 39: 1066-1069.

  26. Naur, Peter (1992), "The Place of Strictly Defined Notation in Human Insight", in Computing: A Human Activity (Addison-Wesley); reprinted in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers, 1993): 261-274.

  27. Nelson, David A. (1992), "Deductive Program Verification (A Practitioner's Commentary)", Minds and Machines 2: 283-307.

  28. Colburn, Timothy R. (1993), "Computer Science and Philosophy", in Timothy R. Colburn, James H. Fetzer, & Terry L. Rankin (eds.), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers): 3-31.

  29. Colburn, Timothy R.; Fetzer, James H.; & Rankin, Terry L. (eds.) (1993), Program Verification: Fundamental Issues in Computer Science (Dordrecht, Holland: Kluwer Academic Publishers).

    • contains a lengthy bibliography

  30. Nelson, David A. (1993), Review of Boyer & Moore's A Computational Logic Handbook and Moore's Special Issue on System Verification (Journal of Automated Reasoning), in Minds and Machines 4: 93-101.

  31. Fetzer, James H. (1993), "Program Verification", in Allen Kent & James G. Williams (eds.), Encyclopedia of Computer Science and Technology, Vol. 28, Supp. 13 (New York: Marcel Dekker): 237-254; reprinted in Allen Kent & James G. Williams (eds.), Encyclopedia of Microcomputers, Vol. 14: Productivity and Software Maintenance: A Managerial Perspective to Relative Addressing (New York: Marcel Dekker): 47-64.

  32. Bowen, J.P., & Hinchey, M.G. (1995), "Ten Commandments of Formal Methods", IEEE Computer 28(4): 56-63.

  33. Glanz, James (1995), "Mathematical Logic Flushes Out the Bugs in Chip Designs", Science 267: 332-333.

  34. Fetzer, James H. (1998), "Philosophy and Computer Science: Reflections on the Program Verification Debate", in Bynum, Terrell Ward; & Moor, James H. (eds.), The Digital Phoenix: How Computers Are Changing Philosophy, Revised Edition (Oxford: Blackwell): 253-273.

  35. Fetzer, James H. (1996), "Computer Reliability and Public Policy: Limits of Knowledge of Computer-Based Systems", Social Philosophy and Policy, forthcoming.

  36. Neumann, Peter (1996, July), "Using Formal Methods to Reduce Risks", Communications of the ACM 39(7): 114.

  37. Pollack, Andrew (1999, May 3), "For Coders, a Code of Conduct: 2000 Problem Tests Professionalism of Programmers", The New York Times: C1, C12.


Copyright © 2004-2007 by William J. Rapaport (rapaport@buffalo.edu)
http://www.cse.buffalo.edu/584/S07/canprogsbeverified.html-20070412