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 Course Materials from Spring 2013 Video of class lectures Lecture Schedule for Spring 2014 Schedule subject to change as course progresses. Lecture slides for not yet given lectures are preliminary, and may change. Jan 22 Course Introduction slides (full sized PDF) (6 up PDF) Jan 24 Review of Propositional Logic slides (full sized PDF) (6 up PDF)   Jan 29 Proof Theory for Propositional Logic slides (full sized PDF) (6 up PDF) Jan 31 Intro to Binary Decision Diagrams (BDDs) slides (full sized PDF) (6 up PDF)   Feb 5 Constructing BDDs slides (full sized PDF) (6 up PDF) Feb 7 Intro to Isabelle slides slides (full sized PDF) (6 up PDF)   Feb 12 Functional Programming in Isabelle slides (full sized PDF), (6 up PDF) theory files my_theory.thy boolexp.thy Feb 14 Functional Programming in Isabelle boolexp.thy continued   Feb 19 First Order Logic slides (full sized PDF) (6 up PDF) Feb 21 First Order Logic - Proofs slides cont from last class   Feb 26 Hoare Logic slides (full sized PDF) (6 up PDF) Feb 28 Hoare Logic (cont) slides (full sized PDF), (6 up PDF)   Mar 5 Hoare Logic in Isabelle slides (full sized PDF) (6 up PDF) theory files Hoare_SIMP.thy Hoare_int_data.thy Hoare_example.thy Mar 7 Hoare Logic in Isabelle slides from last class, theory files Hoare_SIMP.thy Hoare_int_data.thy Hoare_example.thy   Mar 12 Verification Condition Generation slides (full sized PDF) (6 up PDF) theory files Hoare_ann_SIMP.thy Hoare_ann_ex.thy Mar 14 MIDTERM, VCG cont Slides cont   Mar 19 Operational Semantics slides (PPT) (full sized PDF) (6 up PDF) Mar 21 Transition Semantics, Labeled Transition Systems slides(full sized PDF) (6 up PDF)   Mar 26 Spring Break Mar 28 Spring Break   Apr 2 Transition Sementics, Labled Transition Systems Slides cont Apr 4 Labled Transition Systems, Intro to Linear Temporal Logic (LTL) slides slides (full sized PDF)   Apr 9 Class Cancelled Invited to William Mansky's thesis defense Apr 11 Intro to LTL, LTL Semantics slides (Full PDF) (Six Up PDF)   Apr 16 LTL and Model Checking slides (Full PDF) (Six Up PDF) Apr 18 Introduction to SPIN slides (Full PDF) (Six Up PDF)   Apr 23 Promela Syntax slides (Full PDF) (Six Up PDF) Apr 25 Spin Communication slides (Full PDF) (Six Up PDF)   Apr 30 LTL and SPIN Verification slides (Full PDF) (Six Up PDF) slides (Full PDF) (Six Up PDF) May 2 Abstract Interpretation slides (Full PDF) (Six Up PDF)   May 7 Abstract Interpretation slides continued   TBA FINAL TBA