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

- 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

- A Posteriori Verification

Constructive Verification

- R.C. Backhouse.

Prentice-Hall, 1986.

- A.V. Aho and J.D. Ullman.

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.