CS 477: Formal Software Development Methods main  ::  policy  ::  lectures  ::  mps  ::  exams  ::  unit project  ::  resources  ::  faq

Course Materials from Spring 2009 Course Materials from Spring 2010 Course Materials from Spring 2011 Course Materials from Spring 2012 Video of class lectures Lecture Schedule for Spring 2013 Schedule subject to change as course progresses. Lecture slides for not yet given lectures are preliminary, and may change. Jan 16 Course Introduction slides (full sized PDF) (6 up PDF) Jan 18 Review of Propositional Logic slides (full sized PDF) (6 up PDF)   Jan 23 Proof Theory for Propositional Logic slides (full sized PDF) (6 up PDF) Jan 25 Intro to Isabelle/HOL slides (full sized PDF) (6 up PDF)   Jan 30 Intro to Isabelle slides (full sized PDF) (6 up PDF) Feb 1 First Order Logic slides (full sized PDF) (6 up PDF)   Feb 6 FOL cont slides (full sized PDF), (6 up PDF) Feb 8 Hoare Logic slides (full sized PDF), (6 up PDF),   Feb 13 Hoare Logic slides (full sized PDF), (6 up PDF) Feb 15 Hoare Logic (cont) slides from last class, Isabelle thy   Feb 20 Hoare Logic in Isabelle slides (full sized PDF) (6 up PDF) Feb 22 Hoare Logic in Isabelle slides (full sized PDF) (6 up PDF) theory files Hoare_SIMP.thy Hoare_example.thy   Feb 27 Hoare Logic Example slides (full sized PDF) (6 up PDF) theory files Hoare_SIMP.thy Hoare_example.thy Mar 1 Verification Condition Generation slides from last class, theory files Hoare_ann_SIMP.thy Hoare_ann_ex.thy   Mar 6 Operational Semantics slides (PPT) (full sized PDF) (6 up PDF) Mar 8 MIDTERM   Mar 13 Operational Semantics slides (full sized PDF) (6 up PDF) Mar 15 Transition Semantics, Labeled Transition Systems slides(full sized PDF) (6 up PDF)   Mar 20 Spring Break Mar 22 Spring Break   Mar 27 Transition Systems, LTL slides (full sized PDF) (6 up PDF) Mar 29 Intro to Linear Temporal Logic (LTL) slides (Full PDF) (Six Up PDF)   Apr 5 LTL and Model Checking slides (Full PDF) (Six Up PDF) Apr 3 nuSVM slides (Full PDF) (Six Up PDF)   Apr 10 Promela Syntax slides (Full PDF) (Six Up PDF) Apr 12 SPIN Communication slides (Full PDF) (Six Up PDF)   Apr 17 Using SPIN for Verification slides (Full PDF) (Six Up PDF) Apr 19 LTL and SPIN Verification slides (Full PDF) (Six Up PDF)   Apr 24 Abstract Interpretation slides (Full PDF) (Six Up PDF) (Extra slide, pptx) (Extra slide, pdf) Apr 26 Abstract Interpretation slides (Full PDF) (Six Up PDF)   May 1 Abstract Interpretation slides (Full PDF) (Six Up PDF)   TBA FINAL TBA