Next: About this document ...
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
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Dijkstra, Edsger W. (1983), ``Fruits of Misunderstanding'' (EWD-854),
reprinted in Datamation (15 February 1985): 86-87.
- 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.
- Olson, Steve (1984, January/February), ``Sage of Software'',
Science: 75-80.
- 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.
- 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.
- Verity, John W. (1985), ``Bridging the Software Gap,'' Datamation
(15 February): 84, 88.
- 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.
- 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.
- 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.
- 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.
- 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.
- 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.
- Dobson, John; & Randell, Brian (1989), ``Program Verification: Public
Image and Private Reality,'' Communications of the ACM 32: 420-422.
- 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.
- 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.
- Tompkins, Howard E. (1989), ``Verifying Feature-Bugs'' (letter to the
editor), Technical Correspondence, Communications of the ACM 32: 1130-1131.
- Barwise, Jon (1989), ``Mathematical Proofs of Computer System
*]
Correctness,'' Notices of the American Mathematical Society
36: 844-851.
- 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.
- 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.
- 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.
- 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.
- 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.
- Devlin, Keith (1992), ``Computers and Mathematics,'' Notices of the
American Mathematical Society 39: 1065-1066.
- MacKenzie, Donald (1992), ``Computers, Formal Proofs, and the Law
Courts,'' Notices of the
American Mathematical Society 39: 1066-1069.
- 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.
- Nelson, David A. (1992), ``Deductive Program Verification (A
*]
Practitioner's Commentary),'' Minds and Machines 2: 283-307.
- 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.
- 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
- 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.
- 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.
- Bowen, J. P., & Hinchey, M. G. (1995), ``Ten Commandments of Formal Methods'',
*]
IEEE Computer 28(4): 56-63.
- Glanz, James (1995), ``Mathematical Logic Flushes Out the Bugs in Chip
Designs,'' Science 267: 332-333.
- 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).
- Fetzer, James H. (1996), ``Computer Reliability and Public Policy:
*]
Limits of Knowledge of Computer-Based Systems,'' Social Philosophy
and Policy, forthcoming.
- Pollack, Andrew (1999, May 3), ``For Coders, a Code of Conduct: 2000 Problem
Tests Professionalism of Programmers'', The New York Times: C1, C12.
Next: About this document ...
William J. Rapaport
2004-03-03