CSE 3341 2009 Winter
Introduction to Program Verification

Topics: review of formal logic; specifications, programs, and refinement (correctness) as logical expressions; proofs by human and by machine (PVS). Optional topics: semantics of recursion, abstract data types, data refinement, concurrency with communication.

Current Events

Scroll down or click for past and future lecture coverage.

Course Information

instructorAlbert Y. C. Lai lai@cse.yorku.ca
office hoursTuesdays 1:30pm-4:30pm in CSB 2015
textbookA Practical Theory of Programming (online, free)
solutionsThe course has ended and the solutions are offline.
My students: email me
Profs: email me; the department or faculty offices have them on paper too
marking scheme36% four assignments evenly
24% midterm (60 minutes)
40% exam (120 minutes)
due datesA0: Mar 19
A1: Apr 2
midterm: Apr 7
A2: Apr 30
A3: May 14

Lectures Cover These...

1.0Mar 5,10,12
2.0Mar 12
2.2, 2.3Mar 17
3.0, 3.1Mar 19
4.0Mar 26,31
4.1Apr 7,9,14
4.2Apr 16,21,23
PVS introApr 28,30, May 5,7,12
7.2May 14
examplesMay 19

Useful links

More motivation for verification:

Vision of a Grand Challenge project (pdf) by Hoare and Misra.

Software Verification Tools, Chapter 0 (pdf) by Roosen-Runge describes several serious software errors.

Department-Wide Announcements