Can Programs Be Verified?

"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. Turing, Alan M. (1949), "Checking a Large Routine", in Report of a Conference on High Speed Automatic Calculating Machines (Cambridge, UK: University Mathematics Lab): 67-69.
   • Reprinted in:
     Morris, F.L., & Jones, C.B. (1984), "An Early Program Proof by Alan Turing", Annals of the History of Computing 6(2) (April): 139-143.

2. 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.

3. 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.

4. 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.

   ---

5. 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.

   • 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.

   • Shustek, Len (ed.), "An Interview with C.A.R. Hoare", Communications of the ACM 52(3) (March): 38-41.

   • Hoare, C.A.R. (2009), "Retrospective: An Axiomatic Basis for Computer Programming", Communications of the ACM 52(10) (October): 30-32.
     • Humelsine, Jim (2010), "Software Still as Much an Art as Science", Letters to the Editor, Communications of the ACM 53(1) (January): 7; doi:10.1145/1629175.1629178

   ---

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

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

   ---

8. 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.
   • direct access

   • For an interesting contrasting views of the relationship between computer programs and mathematical proofs, see:
     • Thurston, William P. (1994), "On Proof and Progress in Mathematics", Bulletin of the American Mathematical Society 30(2) (April): 161–177.
     • Suber, Peter (1997), "Formal Systems and Machines: An Isomorphism".

   • Another recent article on the nature of proofs, written by a mathematician:
     Stewart, Ian (2007), "The Future of Proof", Prospect (22 February).

   ---

9. 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.

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

11. 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.

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

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

14. 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.

    ---

15. Smith, Brian Cantwell (1985), "Limits of Correctness in Computers", ACM SIGCAS Computers and Society 14-15 (1-4) (January): 18–26; also published as: Technical Report CSLI-85-36 (Stanford, CA: Center for the Study of Language and Information); reprinted 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.
    • If you have trouble loading the paper from the above link,
      click here.

    • The NYTimes report on the moon-missile mistake:
      "Canadian Is Praised over Missile Scare", New York Times (23 December 1960).
    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. 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. 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. On the nature of abstraction, see:

       1. Rapaport, William J. (1999), "Implementation Is Semantic Interpretation" [PDF], The Monist 82 (1): 109-130.
          • This article was based on a longer chapter (which it alludes to as "in preparation"), which has since been published as:
            Rapaport, William J. (2005), "Implementation Is Semantic Interpretation: Further Thoughts", Special Issue on Theoretical Cognitive Science, Journal of Experimental and Theoretical Artificial Intelligence 17(4) (December): 385-417.

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

    6. Dewar, Robert (2009), "CS Education in the U.S.: Heading in the Wrong Direction?", Communications of the ACM 52(7) (July): 41–43.

    7. Morrisett, Greg (2009), "A Compiler's Story", Communications of the ACM 52(7) (July): 106.

    ---

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

17. Myers, Ware (ed.) (1986), "Can Software for the Strategic Defense Initiative Ever Be Error-Free?", [IEEE] Computer (November): 61–67.

18. 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.

    ---

19. 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.
    • direct access
    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.
       • direct access

    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.

20. 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.

21. 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.

22. 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.

23. 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.

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

    ---

25. 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.

26. 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.

27. 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.

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

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

30. 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.

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

32. 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.

33. 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

34. 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.

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

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

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

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

39. Hinchey, Mike; Jackson, Michael; Cousot, Patrick; Cook, Byron; Bowen, Jonathan P.; & Margaria, Tiziana (2008), "Software Engineering and Formal Methods", Communications of the ACM 51(9) (September): 54-59.
    • A recent statement of the argument in favor of program verification.

40. Clarke, Edmund M.; Emerson, E. Allen; & Sifakis, Joseph (2010), "Model Checking: Algorithmic Verification and Debugging", Turing Lecture, Communications of the ACM 52(11) (November): 74–84.