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

Lectures from Spring 2018 Videos of class lectures Transcribed videos class lectures Lecture Schedule for Spring 2020 Schedule subject to change as course progresses. Lecture slides for not yet given lectures are preliminary, and may change. Day Date Topic Slides and Code 1 Jan 22 Course Introduction slides (full sized PDF) (6 up PDF) 2 Jan 24 Review of Propositional Logic slides (full sized PDF) (6 up PDF)   3 Jan 29 Proof Theory for Propositional Logic slides (full sized PDF) (6 up PDF) 4 Jan 31 Soundness of Propositional Proofs slides (full sized PDF) (6 up PDF)   5 Feb 5 Intro to BDDs slides (full sized PDF) (6 up PDF) 6 Feb 7 Construction of BDDs slides (full sized PDF) (6 up PDF) (full sized pic PDF) (6 up pic slides)   7 Feb 12 Introduction to Isabelle slides (full sized PDF), (6 up PDF) theory files my_theory.thy 8 Feb 14 Functional Programming in Isabelle slides (full sized PDF), (6 up PDF) theory files boolexp.thy   9 Feb 19 First Order Logic slides (full sized PDF) (6 up PDF) 10 Feb 21 First Order Logic - Proofs slides cont from last class   11 Feb 26 First Order Logic Proof slides (full sized PDF) (6 up PDF) theory file fol_example 12 Feb 28 Hoare Logic (cont) slides (full sized PDF), (6 up PDF)   13 Mar 4 Hoare Logic in Isabelle slides (full sized PDF) (6 up PDF) theory files lifted_basics lifted_int_predicate_logic lifted_int_data SIMP_syntax.thy Hoare_SIMP.thy Hoare_ex.thy 14 Mar 6 Hoare Logic in Isabelle slides from last class, theory files Hoare_SIMP.thy Hoare_int_data.thy Hoare_ex.thy Hoare_example.thy   15 Mar 11 Verification Condition Generation slides (full sized PDF) (6 up PDF) theory files Hoare_ann_SIMP.thy Hoare_ann_ex.thy 16 Mar 13 Verification Condition Generation, Operational Semantics slides (continued from Mar 11) theory files Hoare_ex.thy   Mar 18 Spring Break Mar 20 Spring Break   17 Mar 25 Natural Semantics slides (full sized PDF) (6 up PDF) theory files SIMP_nat_sem.thy Hoare_sound_and_complete.thy 18 Mar 27 Natural and Transition Sementics slides (full sized PDF) (6 up PDF)   19 Apr 1 Labled Transition Systems slides (full sized PDF) (6 up PDF) 20 Apr 3 Linear Temporal Logic slides (Full PDF) (Six Up PDF)   21 Apr 8 Introduction to Model Checking slides (Full PDF) (Six Up PDF) 22 Apr 10 Buchi Automata slides (Full PDF) (Six Up PDF)   23 Apr 15 LTL Model Checking Alg (1) slides (Full PDF) (Six Up PDF) 24 Apr 17 LTL Model Checking Alg (2) slides   25 Apr 22 LTL and SPIN Verification slides (Full PDF) (Six Up PDF) 26 Apr 24 Abstract Interpretation slides (Full PDF) (Six Up PDF)   27 Apr 29 CFG Standard Interpretation and Abstract Interpretation slides (Full PDF) (Six Up PDF) 28 May 1 Calculating Abstract Interpretations slides (Full PDF) (Six Up PDF)   29 May 6 Abstract Interpretation slides continued   May 12 FINAL 8:00am-10:00am