PROGRAM VERIFICATION

Goals

1. To make students understand the nature of the inherent difficulties of program construction, by making explicit and rigorous the used reasoning processes.
2. To study various techniques of rigorously proving, a posteriori or constructively, that a program meets its specification.

Topics

Why Do We Need Program Verification?
Specifications and Programs
A Brief Introduction to Logic
Proofs by Symbolic Execution
Proofs by Computational Induction:
A Posteriori Verification
Constructive Verification
Proofs by Structural Induction:
A Posteriori Verification
Constructive Verification

Textbook

R.C. Backhouse.
Program Construction and Verification.
Prentice-Hall, 1986.

Other References

A.V. Aho and J.D. Ullman.
Foundations of Computer Science.
Computer Science Press, 1992.

E.W. Dijkstra and W.H.J. Feijen.
A Method of Programming.
Addison-Wesley, 1988.

D. Gries.
The Science of Programming.
Springer-Verlag, 1981.

B. Meyer.
Introduction to the Theory of Programming Languages.
Prentice-Hall, 1988.