Schedule

• Thu, Jan 18:  Motivating examples: Handout 01 slides (click here). Properties of transition systems: Lecture Notes (click here).
  Lecture scribe: Hannah Catabia, lecture notes (pdf file, tex source, png 1, png 2, png 3).
  Assignment 1 and solutions (pdf, pdf), posted Jan 19, due Mon Jan 29.
• Tue, Jan 23:  Finite automata and Buchi automata: Handout 02 slides (click here), Lecture Notes (click here).
  Lecture scribe: Nathan Cordner, lecture notes (pdf file, tex source).
• Thu, Jan 25:  Safety, liveness, invariant properties: Handout 03 slides (click here).
  Lecture scribe: Shreya Ramesh, lecture notes (pdf file, tex source, png).
• Tue, Jan 30:  Regular safety properties: Handout 04 slides (click here).
  Lecture scribe: Ben Gaudiosi, lecture notes (pdf file, tex source).
  Assignment 2 and solutions (pdf, pdf), posted Jan 30, due Wed Feb 07.


• Thu, Feb 01:   Omega-regular properties: Handout 05 slides (click here).
  Lecture scribe: Glib Dolotov, lecture notes (pdf file, tex source).
• Tue, Feb 06:  Linear temporal logic (LTL): Handout 06 slides (click here).
  Lecture scribe: Ruoshi Sun, lecture notes (pdf file, tex source).
  Assignment 3 and solutions (pdf, pdf), posted Feb 06, due Wed Feb 14.
• Thu, Feb 08:  Patterns of specification in LTL: Handout 07 slides (click here), equivalences of LTL formulas: Handout 08 slides (click here) .
  Lecture scribe: Ben Gaudiosi, lecture notes (pdf file, tex source).
• Tue, Feb 13:  Examples in LTL: Handout 09 slides (click here), branching-time temporal logic (CTL): Handout 10 slides (click here).
  Assignment 4 and solutions (pdf, pdf, pdf corrected, courtesy of Daniel Valentine), posted Feb 13, due Wed Feb 21.
• Thu, Feb 15:  CTL semantics, graphically: Handout 11 slides (click here), "dining philosophers" problem: Handout 12 slides (click here), algorithm for CPL model-checking: Handout 13 slides (click here).
  Lecture scribe: Shreya Ramesh, lecture notes (pdf file, tex source, png, png).
• Friday, February 16:  Project proposal due (pdf file of no more than 1-page, not graded).
• Tue, Feb 20:  NO LECTURE. Monday schedule.
  Assignment 5 and solutions (pdf, pdf, pdf courtesy of Nathan Cordner), posted Feb 20, due Wed Feb 28.
• Thu, Feb 22:  Syntax and semantics of CTL*: Handout 14 slides (click here), comparing LTL, CTL, and CTL*: Handout 15 slides (click here).
  Lecture scribe: Glib Dolotov, lecture notes (pdf file, tex source).
• Tue, Feb 27:  More on comparing LTL, CTL, and CTL*.
  Lecture scribe: Wonyl Choi, lecture notes (pdf file, tex source).


• Thu, Mar 01:  
  MidTerm exam and solutions (pdf, pdf) posted Mar 01 at 6:00 pm, due Mar 02 by 6:00 pm.


• Saturday, March 03 -- Sunday, March 11:  SPRING RECESS.


• Tue, Mar 13:   Lecture cancelled because of snow storm.
  Assignment 6 and solutions (pdf, pdf, Problem 3 graded, courtesy of Daniel Valentine), posted Mar 13, due Wed Mar 21.
• Thu, Mar 15:   Hoare Logic: Handout 16 slides (click here), Hoare Logic (continued): Handout 17 slides (click here).
  Lecture scribe: Hannah Catabia, lecture notes (pdf file, tex source)
• Tue, Mar 20:  Hoare Logic (continued): Handout 18 slides (click here), Hoare Logic (continued): Handout 19 slides (click here).
  Lecture scribe: Ben Gaudiosi, lecture notes (pdf file, tex source)
• Thu, Mar 22:  Hoare Logic (continued): Handout 20 slides (click here).
  Lecture scribe: Nathan Cordner, lecture notes (pdf file, tex source).
  Assignment 7 and solutions (pdf, pdf, Problem 3 graded, courtesy of Nathan Cordner), posted Mar 22, due Fri Mar 30.
• Tue, Mar 27:  Hoare Logic and variations: Lecture Notes (click here).
• Thu, Mar 29:  Hoare Logic and variations (updated): Lecture Notes (click here).
  Lecture scribe: Glib Dolotov, lecture notes (pdf file, tex source).
  Assignment 8 and solutions (pdf, pdf, pdf, pdf, Problems 1 and 5 graded, solutions for Problem 5 due to Nathan Cordner, Wonyl Choi, and Daniel Valentine), posted Mar 29, due Fri Apr 06.


• Tue, Apr 03:  Alley Stoughton's lecture I on EasyCrypt, lecture slides (click here).
• Thu, Apr 05:  Alley Stoughton's lecture II on EasyCrypt.
  Lecture scribe: Yara Awad, lecture notes (pdf file).
  Assignment 9 and solutions (pdf, pdf, ec, Problem 1 graded by Daniel Valentine, solution courtesy of Yara Awad), posted Apr 06, due Fri Apr 13.
• Tue, Apr 10:  Alley Stoughton's lecture III on EasyCrypt.
• Thu, Apr 12:  Probabilistic CTL: Handout 21 slides (click here). Lecture scribe: Hannah Catabia, lecture notes (pdf file).
  Assignment 10 and solutions (pdf, pdf, pdf, docx, Problems 2 and 5 graded by Yara Awad, solutions for Problem 2 due to Nathan Cordner and Daniel Valentine, solutions for Problem 5 due to Alley Stoughton), posted Apr 13, due Fri Apr 20.
• Tue, Apr 17:  Counterexamples and probabilistic model-checking: Handout 22 slides (click here).
• Thu, Apr 19:  Counterexamples and probabilistic model-checking (continued). Adding probability to a formal logic: Lecture Notes (click here).
  Assignment 11 and solutions (pdf, pdf, Problem 3 graded by Yara Awad, solution due to Hannah Catabia), posted Apr 20, due Fri Apr 27.
• Tue, Apr 24:  Modal logics: Handout 23 slides (click here).
• Thu, Apr 26:  Modal logics (continued).


• Tue, May 01:  What is first-order modal logic?: Lecture Notes (click here).


• Friday, May 04:  Term project due.
• End-of-term exam and solutions ( pdf, pdf), posted Tuesday, May 08, at 12:00 noon, due Wednesday, May 09 by 12:00 noon.