COSC 3341 3.0 Introduction to Program Verification

Winter 2001

Section M


Brief overview

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 include the use of simple tools to aid in verification.

Topics covered will include the following:

General information

Time: Monday, Wednesday and Friday, 12:30-13:30
Place: CCB 115
Instructor: Franck van Breugel
Office hours: Monday, Wednesday and Friday, 13:30-14:30 or by appointment
Office: CCB 348
Prerequisites: general prerequisites, including MATH 2090
Degree credit exclusion: COSC 3111

Reference material

The text for the course is The files are in PDF and PostScript format. For information on how to print them, and how to conserve paper, see the Ariel printing FAQ. Some corrections can be found here.

The following book is suggested for further reading.

This book is on reserve in the Steacie library.


The student's performance in the course will be evaluated as a combination of a final exam (50%), a midterm (30%) and assignments (20%). More details are given below. There will be no supplemental examination for the course. Neither will students have the option of doing additional work to upgrade their mark.


There will be two assignments. These assignments are given out on
  1. March 12 and
  2. April 16.
The assignments should be handed in within two weeks. No late assignments will be accepted. If a student cannot hand in the assignment in time for reasons beyond his/her control, the student should bring a documented note to the instructor. If accepted, the weight of the other assignment will be prorated accordingly. The assignments will be returned within two weeks after the due date. Each assignment is worth 10%.


The midterm will be held on April 2. The midterm will be written in class. If a student misses the midterm for reasons beyond his/her control, the student has to bring a documented note to the instructor. If accepted, the weight of the final exam will be prorated accordingly.

Final exam

The final exam will be held in the examination period. It will be a two hour exam.


The suggested reading material and additional material can be found by clicking on the corresponding date on the calendar below.

Course outline in PostScript and PDF