PROGRAM VERIFICATION:

A PARTIAL BIBLIOGRAPHY IN CHRONOLOGICAL ORDER

William J. Rapaport

Department of Computer Science and Center for Cognitive Science State University of New York at Buffalo, Buffalo, NY 14260

                   rapaport@cse.buffalo.edu
            http://www.cse.buffalo.edu/∼rapaport/

March 3, 2004

* 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. De Millo, Richard A.; Lipton, Richard J.; & Perlis, Alan J. (1979), “Social Processes and Proofs of Theorems and Programs,” Communications of the ACM 22: 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.

* 6. 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.

7. Dijkstra, Edsger W. (1983), “Fruits of Misunderstanding” (EWD-854), reprinted in Datamation (15 February 1985): 86–87.

* 8. 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.

9. Olson, Steve (1984, January/February), “Sage of Software”, Science: 75–80.

* 10. 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.

** 11. Smith, Brian Cantwell (1985), “Limits of Correctness in Computers,” 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; eprinted 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.

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

* 13. 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.

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

** 15. Fetzer, James H. (1988), “Program Verification: The Very Idea,” Communications of the ACM 31: 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.

(a) 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: 287–290.

(b) 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: 374–377.

(c) Fetzer, James H. (1989), “Program Verification Reprise: The Author’s Response” (to the above 5 letters), Technical Correspondence, Communications of the ACM 32: 377-381.

(d) Dobson, John; & Randell, Brian (1989), “Program Verification: Public Image and Private Reality,” Communications of the ACM 32: 420–422.

(e) 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: 506–512.

(f) 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: 790–792.

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

* 16. Barwise, Jon (1989), “Mathematical Proofs of Computer System Correctness,” Notices of the American Mathematical Society 36: 844–851.

(a) 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.

* 17. 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.

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

* 19. 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.

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

21. Devlin, Keith (1992), “Computers and Mathematics,” Notices of the American Mathematical Society 39: 1065–1066.

22. MacKenzie, Donald (1992), “Computers, Formal Proofs, and the Law Courts,” Notices of the American Mathematical Society 39: 1066–1069.

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

* 24. Nelson, David A. (1992), “Deductive Program Verification (A Practitioner’s Commentary),” Minds and Machines 2: 283–307.

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

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

* 28. 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.

* 29. Bowen, J. P., & Hinchey, M. G. (1995), “Ten Commandments of Formal Methods”, IEEE Computer 28(4): 56–63.

30. Glanz, James (1995), “Mathematical Logic Flushes Out the Bugs in Chip Designs,” Science 267: 332– 333.

* 31. Fetzer, James H. (1995), “Philosophy and Computer Science: Reflections on the Program Verification Debate,” paper presented at the American Philosophical Association Central Division meeting, Chicago (April 1995).

* 32. Fetzer, James H. (1996), “Computer Reliability and Public Policy: Limits of Knowledge of Computer-Based Systems,” Social Philosophy and Policy, forthcoming.

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