Department of Computer Science

Course director: J. Ostroff
Implementation details

COSC 3111.03 Introduction to Program Verification

Section M  Winter       Mon, Wed 11:30-13:00

Every program implicitly asserts a theorem to the effect that if certain input conditions are met then the program will do what its specifications or documentation says it will. Making that theorem true is not merely a matter of luck or patient debugging; making a correct program can be greatly aided by a logical analysis of what it is supposed to do, and for small pieces of code a proof that the code works can be produced hand-in-hand with the construction of the code itself. Good programming style works in part because it makes the verification process easier and this in turn makes it easier to develop more complex algorithms from simple ones.

The course will provide an introduction to the basic concepts of formal verification methods. It will also including the use of simple tools to aid in verification.

Topics covered may include the following.

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

Suggested readings:

Prerequisites: general prerequisites, including MATH2090.03