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

Video of class lectures Lecture Schedule for Spring 2018 Schedule subject to change as course progresses. Lecture slides for not yet given lectures are preliminary, and may change. Jan 17 Course Introduction slides (full sized PDF) (6 up PDF) Jan 19 Review of Propositional Logic slides (full sized PDF) (6 up PDF)   Jan 24 Proof Theory for Propositional Logic slides (full sized PDF) (6 up PDF) Jan 26 Soundness of Propositional Proofs slides (full sized PDF) (6 up PDF) (annotated slides PDF)   Jan 31 Intro to BDDs slides (full sized PDF) (6 up PDF) Feb 2 Construction of BDDs slides slides (full sized PDF) (6 up PDF) (annotated slides)   Feb 7 Introduction to Isabelle slides (full sized PDF), (6 up PDF) theory files my_theory.thy Feb 9 Functional Programming in Isabelle (full sized PDF), (6 up PDF) theory files boolexp.thy   Feb 14 First Order Logic slides (full sized PDF) (6 up PDF) Feb 16 First Order Logic - Proofs slides cont from last class   Feb 21 First Order Logic Proof slides (full sized PDF) (6 up PDF) Feb 23 Hoare Logic (cont) slides (full sized PDF), (6 up PDF)   Feb 28 Hoare Logic in Isabelle slides (full sized PDF) (6 up PDF) theory files Hoare_SIMP.thy Hoare_int_data.thy Hoare_ex.thy Mar 2 Hoare Logic in Isabelle slides from last class, theory files Hoare_SIMP.thy Hoare_int_data.thy Hoare_example.thy   Mar 7 Verification Condition Generation slides (full sized PDF) (6 up PDF) theory files Hoare_ann_SIMP.thy Hoare_ann_ex.thy Mar 9 MIDTERM, EOH   Mar 14 Verification Condition Generation, Operational Semantics slides (full sized PDF) (6 up PDF) Mar 16 Transition Semantics, Labeled Transition Systems slides(full sized PDF) (6 up PDF)   Mar 21 Spring Break Mar 23 Spring Break   Mar 28 Transition Sementics, Labled Transition Systems slides(full sized PDF) (6 up PDF) Mar 30 Labled Transition Systems, Intro to Linear Temporal Logic (LTL) slides slides (full sized PDF) (6 up PDF)   Apr 4 Linear Temporal Logic slides (Full PDF) (Six Up PDF) Apr 6 Introduction to SPIN slides (Full PDF) (Six Up PDF)   Apr 11 Promela Syntax slides (Full PDF) (Six Up PDF) Apr 13 Introduction to Executing SPIN slides (Full PDF) (Six Up PDF)   Apr 18 LTL and SPIN Verification slides (Full PDF) (Six Up PDF) Apr 20 Abstract Interpretation slides (Full PDF) (Six Up PDF)   Apr 25 CFG Standard Interpretation and Abstract Interpretation slides (Full PDF) (Six Up PDF) Apr 27 Calculating Abstract Interpretations slides (Full PDF) (Six Up PDF)   May 2 Abstract Interpretation slides continued   May 10 FINAL TBA