15-819A3 Specification, Verification, and Refinement of Software

15-819A3 Specification, Verification, and Refinement of Software (6 units) Spring 2003

John C. Reynolds

First Half of Spring Semester 2003

Tuesdays and Thursdays, 1:30-2:50 pm Wean Hall 4601

Course Description

Specification and verification of imperative programs, using the methods of Floyd, Hoare, and Dijkstra, and of the refinement calculus. Emphasis will be on the application to realistic programs. We hope to demonstrate verification techniques using an implementation of Hoare logic (by T. Nipkow) in Isabelle/HOL.

PREREQUISITES: Open to all CMU MS and PhD students. Undergraduates by permission of the instructor.

TEXT: Notes and papers will be distributed.

METHOD OF EVALUATION: Grading will be based on homework and final exam.

Class Notes (in Postscript)

Expressions, Commands, and Assertions, revised January 20

Specifications and Their Inference Rules, revised January 28

Arrays, revised February 13

Procedures, revised February 25

Additional Topics, revised February 25

Homework (in Postscript)

Homework 1, January 23, 2003, due January 30

Homework 2, February 11, 2003, due February 18

Homework 3, February 20, 2003, due February 27

Tentative Bibliography

Floyd, Robert W. Assigning Meanings to Programs. Mathematical Aspects of Computer Science, American Mathematical Society 1967, pp. 19-32.
Hoare, C. A. R., An Axiomatic Basis for Computer Programming. CACM 12, October 1969, pp. 576-580 and 583.
Hoare, C. A. R., Proof of a Program: FIND. CACM 14, January 1971, pp. 39-45.
Hoare, C. A. R., Towards a Theory of Parallel Programming. Operating Systems Techniques, ed. C. A. R. Hoare and R. H. Perrott, Academic Press 1972, pp. 61-71.
Owicki, Susan S. and Gries, David, Verifying Properties of Parallel Programs: An Axiomatic Approach. CACM 19, May 1976, pp. 279-285.
Dijkstra, Edsger W., Guarded Commands, Nondeterminacy and Formal Derivation of Programs. CACM 18, August 1975, pp. 453-457.
Reynolds, John C., The Craft of Programming, Prentice-Hall International 1981, chapters 1, 2, and 5.
Necula, George C., Proof-Carrying Code. POPL 24, January 1997, pp. 106-119.
Nipkow, Tobias, Paulson, Lawrence C., and Wenzel, Marcus, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS 2283 , 2002.
Reynolds, John C., Separation Logic: A Logic for Shared Mutable Data Structures. LICS 17, July 2002.

last updated March 27, 2003