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.
Scroll down or click for past and future lecture coverage.
| instructor | Albert Y. C. Lai lai@cse.yorku.ca |
|---|---|
| office hours | Tuesdays 1:30pm-4:30pm in CSB 2015 |
| textbook | A Practical Theory of Programming (online, free) |
| solutions | The 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 scheme | 36% four assignments evenly 24% midterm (60 minutes) 40% exam (120 minutes) |
| due dates | A0: Mar 19 A1: Apr 2 midterm: Apr 7 A2: Apr 30 A3: May 14 |
| Section | Date |
|---|---|
| 1.0 | Mar 5,10,12 |
| 2.0 | Mar 12 |
| 2.2, 2.3 | Mar 17 |
| 3.0, 3.1 | Mar 19 |
| 4.0 | Mar 26,31 |
| 4.1 | Apr 7,9,14 |
| 4.2 | Apr 16,21,23 |
| PVS intro | Apr 28,30, May 5,7,12 |
| 7.2 | May 14 |
| examples | May 19 |
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.
None.