Archived Announcements
[Click here for current announcements.]
| Date | Topic | Description |
|---|---|---|
| Tue 8/31 | HW1 | HW1 is available in CMS, due Thursday 9/9. You may work with a partner. If you do, please form a group in CMS. Only one of you needs to submit the solutions. |
| Tue 9/7 | Office hours | PLDG has been scheduled on top of my Tuesday office hours, so I will just shift them to Wednesday unless there are objections. So my new hours are Wednesday and Thursday 1:15–2:30pm. In addition, you are always welcome to drop in anytime I am here. |
| Tue 9/7 | Hoare Logic | Here is an old survey paper of Apt on Hoare Logic. |
| Thu 9/9 | HW2 | HW2 is available in CMS, due Thursday 9/23. You may work with a partner. If you do, please form a group in CMS. Only one of you needs to submit the solutions. |
| Fri 9/17 | HW2 erratum | The definition of atomic in Ex. 2 should read: a Boolean algebra is atomic if there are no nonzero atomless elements. |
| Fri 9/17 | Homework partners | If anyone who submitted HW1 alone would prefer to work with a partner in the future, please let me know. I will try to match you up. |
| Thu 9/23 | HKT Ch. 4-10 | Here are the chapters of HKT that deal with PDL. |
| Thu 9/23 | HW3 | HW3 is available in CMS, due Thursday 10/7. Partners allowed as usual, but please form a group in CMS. |
| Tue 10/5 | No class 10/7 | Lecture is canceled for Thursday 10/7, as I have to cover for Ramin Zabih in 3110. Also, no lecture Tuesday 10/12 due to fall break. See you Thursday 10/14. |
| Wed 10/13 | Guest lecture 10/14 | Olivier Danvy, University of Aarhus, will give a guest lecture on Thursday, 10/14 entitled ``A walk in the semantic park.'' |
| Thu 10/14 | Guest lecture 10/15 | Olivier will give the second half of his lecture tomorrow, Friday 10/15, 3:45pm, 211 Upson (unless you hear otherwise—watch this space). |
| Thu 10/14 | Office hours | Dexter's office hours are canceled today due to hosting responsibilities. |
| Sun 10/17 | HW4 | HW4 is available in CMS, due Thursday 10/28. Partners allowed as usual, but please form a group in CMS. |
| Tue 11/9 | Notes on PPDL | Notes on probabilistic PDL are available here. |
| Tue 11/9 | No class Thursday 11/11 | Class is canceled for this Thursday 11/11, as I will be in NYC at a workshop. See you next Tuesday. |
| Wed 11/10 | HW5 | HW5 (the last!) is available in CMS, due Tuesday 11/30. Partners allowed as usual, please form a group in CMS. |
| Wed 11/10 | HKT Ch. 11-17 | Here are the remaining chapters of HKT. |
| Tue 10/19 | Final Projects | Please send me your proposals for final projects by the end of next week. Options are: (i) a 10-page survey paper on some topic related to program logic and verification (e.g., model checking, type theory, probabilistic verification); (ii) a programming project implementing some decision procedure or proof system, or a nontrivial verification exercise using an off-the-shelf system such as Coq or Nuprl; (iii) a take-home final exam. |
| Wed 11/24 | Office hours canceled | I have to cancel my office hours today for a doctor appointment. |
| Tue 11/30 | Handouts | I have posted some papers on model checking for the mu-calculus and parity games. |