Dr. Jim Sasaki, CS Dept., Illinois Institute of Technology
For posted grades and lecture videos, go to Blackboard.
| Date | Activity | Assignment Due | Topic |
|---|---|---|---|
| Monday Aug 24 | Lec 1 | Welcome | About Active Learning | Activity: Why Verify? (& Responses) | Notes: Parallel Programs Are Hard To Understand; Review Propositional logic | Activity: Sample Formal System (v1.1) | Postmorterm | |
| Aug 31 | Lec 2 | Complete Activity: Sample Formal System | HW 01: Propositional Logic (Pre-class | Post-class) | Notes (Pre | Post) | Activity: Revisiting Robs (Pre | Post) | Activity: Predicate Logic (Pre | Post) |
| Sep 7 | Labor Day Holiday (No class) | ||
| Sep 14 | Lec 3 | HW 02 (Part 1): | Notes: (Pre | Post)-class Notes: Meanings of Expressions (& Activity) | State updating (& Activity) | Review for Quiz 1 (updated to v.1.1) | Postmortem |
| Sep 21 | Quiz 1 (30 min) | On material < Statements (i.e., ≤ State Updating) | Solution | |
| Lec 4 | Notes: (Pre | Post)-class: Statements, Programs, Hoare Triples; Activities: (Simple Programs | Program Meanings, Satisfaction, Triples) | ||
| Sep 28 | Lec 5 | HW 03: Problems 3-10 of Activity: Program Meanings, Satisfaction, Triples (solution) | Quiz 1 Results | Notes (Pre | Post)-class: Syntactic Substitution & Proof Rules | Activities (Substitution | Proof Rules) | Review for Quiz 2 |
| Oct 5 | Quiz 2 (30 min) | On Syntax/Semantics of Statements and Programs (in our Deterministic Language); Partial Correctness Triples and their Satisfaction; and Syntactic Substitution. (Review) | |
| Lec 6 | Notes: Proof Rules and Proof Outlines (updated) | Activity: Simple Proofs | Activity: Proof Outlines | ||
| Oct 12 | Fall Break (No class) | ||
| Oct 19 | Lec 7 | Quiz 2 Results | Notes (updated Oct 26) (Verification Examples; Partial Proof Outlines; Forward Assignment) | Activity: Simple Proofs | Exam 2 Review | |
| Oct 26 | Midterm Exam (60 min) | Material ≤ Lecture 6 (apx. half on proof rules and proof outlines, half on earlier material). | |
| Lec 8 | Notes: More Assignment Rules, Loop Examples | Activity | ||
| Nov 2 | Lec 9 | Midterm solution | Notes (Termination and wp) | Activity: Loop Bounds | Activity: Weakest Preconditions (do as HW for next week) | |
| Nov 9 | Lec 10 | HW 04: Weakest Preconditions (Activity from last week)| HW 04 Solution | Notes: Finding Invariants | Array Asgts | Activity: Upcoming Quizzes? Finding Invariants |
| Nov 16 | |||
| Nov 16 | Lec 11 | HW 05: Array Assignments | Quiz 3 Review (Solution) | Disjoint Parallel Programs & Evaluation Graphs (Notes | Activity) |
| (Nov 18) | Solutions to Activities from Classes 7—9 | Solution to Quiz 3 Review | ||
| Nov 23 | Quiz 3 (30 min) [moved here] | Lectures 7—9 | |
| Nov 23 | Lec 12 | ||
| Nov 30 | |||
| Lec 13 | |||
| Dec 7* | Lec 14 | ||
| Mon Dec 14 (7:30 pm - 9:30 pm) (See the Fall 2009 Final Exam Schedule) | Final Exam (Comprehensive) | ||
*(If you're in the Wed CS 542 section, see the instructor about taking the CS 542 final exam just before lecture on December 7.)
Sun Aug 16: Textbook (required): Verification of Sequential and Concurrent Programs (2nd edition), by Krzysztof R. Apt and Ernst-Rüdiger Olderog, ©1997, Springer-Verlag, ISBN 0387948961.
A well-respected reference book is The Science of Programming, by David Gries, Springer-Verlag, © 1987, ISBN 0387964800.